lean2/tests/lean/unfoldf.lean

29 lines
484 B
Text
Raw Normal View History

open nat
-- definition id [unfold_full] {A : Type} (a : A) := a
definition compose {A B C : Type} (g : B → C) (f : A → B) (a : A) := g (f a)
notation g ∘ f := compose g f
example (a b : nat) (H : a = b) : id a = b :=
begin
esimp,
state,
exact H
end
example (a b : nat) (H : a = b) : (id ∘ id) a = b :=
begin
esimp,
state,
exact H
end
attribute compose [unfold_full]
example (a b : nat) (H : a = b) : (id ∘ id) a = b :=
begin
esimp,
state,
exact H
end