michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/elaborator): use is_convertible for constraints without metavariables in the elaborator

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-01 03:14:01 -08:00
parent cbd1f98365
commit 5f29146e0b
2 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/lean/ex4.lean
View file

@ -2,7 +2,7 @@ Import tactic
Import int
Definition a : Nat := 10
(* Trivial indicates a "proof by evaluation" *)
Theorem T1 : a > 0 := (by trivial)
Theorem T2 : a - 5 > 3 := (by trivial)
Theorem T1 : a > 0 := Trivial
Theorem T2 : a - 5 > 3 := Trivial
(* The next one is commented because it fails *)
(* Theorem T3 : a > 11 := Trivial *)

10
src/library/elaborator/elaborator.cpp
View file

@ -1300,6 +1300,16 @@ class elaborator::imp {
bool eq = is_eq(c);
if (a == b)
return true;
if (!has_metavar(a) && !has_metavar(b)) {
if (!eq) {
if (m_type_inferer.is_convertible(a, b, ctx)) {
return true;
} else {
m_conflict = justification(new unification_failure_justification(c));
return false;
}
}
}
if (process_assigned_metavar(c, a, true) || process_assigned_metavar(c, b, false))
return true;