2014-10-03 00:42:33 +00:00
|
|
|
import logic
|
|
|
|
|
|
|
|
|
|
|
2014-10-09 14:13:06 +00:00
|
|
|
context
|
2014-10-03 00:42:33 +00:00
|
|
|
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
|
