repeat
repeat は、指定したタクティクを失敗するまで繰り返します。
variable (P Q R S T : Prop)
example : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by
repeat intro
repeat apply_assumption
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help
repeat は、指定したタクティクを失敗するまで繰り返します。
variable (P Q R S T : Prop)
example : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by
repeat intro
repeat apply_assumption