2015-12-03 00:44:21 +00:00
|
|
|
constant P : nat → Prop
|
|
|
|
|
|
2015-12-03 03:23:41 +00:00
|
|
|
lemma tst₀ [forward] : ∀ x, P x := -- Fine
|
|
|
|
|
sorry
|
|
|
|
|
|
2015-12-03 00:44:21 +00:00
|
|
|
lemma tst₁ [forward] : ∀ x, (: P x :) := -- Fine
|
|
|
|
|
sorry
|
|
|
|
|
|
|
|
|
|
lemma tst₂ [forward] : ∀ x, P (: x :) := -- Error
|
|
|
|
|
sorry
|
2015-12-03 03:23:41 +00:00
|
|
|
|
|
|
|
|
lemma tst₃ [forward] : ∀ x, P (: id x :) :=
|
|
|
|
|
sorry
|
|
|
|
|
|
|
|
|
|
reveal tst₀ tst₁ tst₃
|
|
|
|
|
print tst₀
|
|
|
|
|
print tst₁
|
|
|
|
|
print tst₃
|
2015-12-03 06:36:10 +00:00
|
|
|
|
|
|
|
|
definition tst₄ [forward] : ∀ x : nat, (: id x :) = x :=
|
|
|
|
|
λ x, rfl
|
