lean2/tests/lean/exact_partial.lean

6 lines
91 B
Text
Raw Permalink Normal View History

example (a b : Prop) : a → b → a ∧ b :=
begin
intros,
exact (and.intro _ _),
end