Skip to content

Commit

Permalink
Revert "test: Basic を解く"
Browse files Browse the repository at this point in the history
This reverts commit 70a25d4.
  • Loading branch information
Seasawher committed Feb 20, 2024
1 parent 914062c commit 19b711e
Showing 1 changed file with 3 additions and 6 deletions.
9 changes: 3 additions & 6 deletions Tutorial/Basic/Lecture1.lean
Original file line number Diff line number Diff line change
Expand Up @@ -41,20 +41,17 @@ variable (P Q R : Prop)

example (hP : P) : P := by
-- ヒント: `apply hP`と入力すれば仮定をゴールに適用できる。
assumption
sorry

example (h : P → Q) (hP : P) : Q := by
-- 改行して複数のtacticを並べることもできる。インデント(行の頭の空白の個数)を
-- 揃える必要があることに注意しよう。
-- ヒント: `apply`を2回使う。
repeat apply_assumption
sorry

example (h : P → Q) (h' : Q → R) : P → R := by
-- ヒント: `intro hP`と入力すれば仮定`hP : P`が得られる。
intro hP
apply h'
apply h
assumption
sorry

-- TIPS: 入力した`intro`や`apply`の上にカーソルを乗せるとtacticの説明が表示される。

Expand Down

0 comments on commit 19b711e

Please sign in to comment.