max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/parser): fixes #1290

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-09 15:35:25 -08:00
parent b526e30c55
commit 7d540b6d02
3 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/parser.cpp
View file

@ -966,6 +966,10 @@ bool parser::parse_binder_collection(buffer<pair<pos_info, name>> const & names,
notation::accepting const & acc = head(acc_lst);
lean_assert(!acc.get_postponed());
expr pred = acc.get_expr();
auto k = p.first.get_action().kind();
if (k == notation::action_kind::Skip ||
k == notation::action_kind::Ext)
return false;
unsigned rbp = p.first.get_action().rbp();
next(); // consume tk
expr S = parse_expr(rbp);

12
tests/lean/1290.lean Normal file
View file

@ -0,0 +1,12 @@
structure Category :=
(Obj : Type)
(Hom : Obj -> Obj -> Type)
structure Isomorphism ( C: Category ) { A B : C^.Obj } :=
(morphism : C^.Hom A B)
instance Isomorphism_coercion_to_morphism { C : Category } { A B C^.Obj } : has_coe (Isomorphism C A B) (C^.Hom A B) :=
(coe: Isomorphism.morphism)
instance Isomorphism_coercion_to_morphism_fixed { C : Category } { A B : C^.Obj } : has_coe (Isomorphism C) (C^.Hom A B) :=
{coe := Isomorphism.morphism}

1
tests/lean/1290.lean.expected.out Normal file
View file

@ -0,0 +1 @@
1290.lean:8:66: error: invalid declaration, '}' expected