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

fix(frontends/lean/structure_cmd): internal name of parameter/variable was being erased

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-23 15:01:27 -08:00
parent 7d35d18cad
commit 75acb3bc66
2 changed files with 15 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/structure_cmd.cpp
View file

@ -274,7 +274,8 @@ struct structure_cmd_fn {
*/ */
expr update_locals(expr new_tmp, buffer<expr> & locals) { expr update_locals(expr new_tmp, buffer<expr> & locals) {
for (unsigned i = 0; i < locals.size(); i++) { for (unsigned i = 0; i < locals.size(); i++) {
expr new_local = mk_local(binding_name(new_tmp), binding_domain(new_tmp), binding_info(new_tmp)); expr new_local = mk_local(mlocal_name(locals[i]), binding_name(new_tmp), binding_domain(new_tmp),
binding_info(new_tmp));
locals[i] = new_local; locals[i] = new_local;
new_tmp = instantiate(binding_body(new_tmp), new_local); new_tmp = instantiate(binding_body(new_tmp), new_local);
} }

13
tests/lean/hott/443.hlean Normal file
View file

@ -0,0 +1,13 @@
import algebra.group algebra.precategory.basic algebra.precategory.morphism
open eq sigma unit precategory morphism path_algebra
context
parameters {P₀ : Type} [P : precategory P₀]
structure my_structure := (a : P₀) (b : P₀) (f : @hom P₀ P a b)
include P
structure another_structure (X : my_structure) := (field1 : hom (my_structure.a X) (my_structure.a X))
end