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

fix(library/tmp_type_context): bug at pop()

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-05 19:14:33 -08:00
parent df567717f8
commit 6193816f6a
2 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/tmp_type_context.cpp
View file

@ -135,6 +135,7 @@ void tmp_type_context::pop() {
lean_assert(m_trail.size() == old_sz);
m_uassignment.resize(s.m_uassignment_sz);
m_eassignment.resize(s.m_eassignment_sz);
m_scopes.pop_back();
}
void tmp_type_context::commit() {

17
tests/lean/run/blast_ematch_uni_issue.lean Normal file
View file

@ -0,0 +1,17 @@
set_option blast.ematch true
variable {A : Type}
definition R : A → A → Prop := sorry
definition R_trans [forward] {a b c : A} : R a b → R b c → R a c := sorry
example (a b c : A) : R a b → R b c → R a c :=
by blast
example {A : Type} (a b c : A) : R a b → R b c → R a c :=
by blast
example {A : Type.{1}} (a b c : A) : R a b → R b c → R a c :=
by blast
universe u
example {A : Type.{u}} (a b c : A) : R a b → R b c → R a c :=
by blast