lean2/tests/lean/exact_partial2.lean

5 lines
99 B
Text
Raw Permalink Normal View History

example (a b c : nat) (h₁ : a = b) (h₂ : b = c) : a = c :=
begin
exact (eq.trans h₁ _)
end