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

fix(library/unifier): typo

Browse source 
fixes #588
This commit is contained in:
Leonardo de Moura 2015-05-07 16:17:38 -07:00
parent 88cd6e9a63
commit eb3a236119
2 changed files with 21 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/unifier.cpp
View file

@ -1359,7 +1359,7 @@ struct unifier_fn {
expr rhs_fn = get_app_rev_args(rhs, rhs_args);
declaration d = *m_env.find(const_name(lhs_fn));
levels lhs_lvls = const_levels(lhs_fn);
levels rhs_lvls = const_levels(lhs_fn);
levels rhs_lvls = const_levels(rhs_fn);
if (length(lhs_lvls) != length(rhs_lvls) ||
d.get_num_univ_params() != length(lhs_lvls)) {
// the constraint is not well-formed, this can happen when users are abusing the API

20
tests/lean/run/588.lean Normal file
View file

@ -0,0 +1,20 @@
import standard
open function
variables {a b r : Type}
definition f a := Πr, (a -> r) -> r
definition g (fn : a -> b) (sa : f a) : f b := sorry
-- ok
check λx, g id x = x
check λ(x : f a), g id x = x
universe variables l₁ l₂ l₃
check λ (x : f.{_ l₂} a), g.{_ _ l₂ l₂} id x = x
example (x : f a) : g id x = x :=
sorry