lean2/tests/lean/var2.lean

15 lines
186 B
Text
Raw Normal View History

import logic
context
universe l
variable A : Type.{l}
variable a : A
parameter B : Type.{l}
parameter b : B
definition foo := fun (H : A = B), cast H a = b
end
check foo