4dd6cead83
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.
- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
l = nil
will not propagate the type (List Int) to nil.
- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.
Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
29 lines
673 B
Text
29 lines
673 B
Text
|
|
|
|
Variable f {A : Type} (a b : A) : A.
|
|
Check f 10 true
|
|
|
|
Variable g {A B : Type} (a : A) : A.
|
|
Check g 10
|
|
|
|
Variable h : Pi (A : Type), A -> A.
|
|
|
|
Check fun x, fun A : Type, h A x
|
|
|
|
Variable my_eq : Pi A : Type, A -> A -> Bool.
|
|
|
|
Check fun (A B : Type) (a : _) (b : _) (C : Type), my_eq C a b.
|
|
|
|
Variable a : Bool
|
|
Variable b : Bool
|
|
Variable H : a /\ b
|
|
Theorem t1 : b := Discharge (fun H1, Conj H1 (Conjunct1 H)).
|
|
|
|
Theorem t2 : a = b := Trans (Refl a) (Refl b).
|
|
|
|
Check f Bool Bool.
|
|
|
|
Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a :=
|
|
Discharge (λ H, DisjCases (EM a)
|
|
(λ H_a, H)
|
|
(λ H_na, NotImp1 (MT H H_na)))
|