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

fix(frontends/lean/scanner): wrong upos after field projection

Browse source
This commit is contained in:
Sebastian Ullrich 2017-05-23 10:33:31 +02:00
parent 5d6bf38b7e
commit 5a19430f60
3 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -523,7 +523,7 @@ auto scanner::read_key_cmd_id() -> token_kind {
break;
}
}
move_back(cs.size() - id_sz, num_utfs - 1);
move_back(cs.size() - id_sz, 1);
cs.shrink(id_sz);
cs.push_back(0);
m_name_val = name(cs.data());
@ -531,7 +531,6 @@ auto scanner::read_key_cmd_id() -> token_kind {
}
}
} else if (is_id_first(cs, 0)) {
id_sz = cs.size();
while (true) {
id_sz = cs.size();
id_utf_sz = num_utfs;

2
tests/lean/field_proj_pos.lean Normal file
View file

@ -0,0 +1,2 @@
example (h : true ∨ true) : true :=
by exact (h).elim _ _

7
tests/lean/field_proj_pos.lean.expected.out Normal file
View file

@ -0,0 +1,7 @@
field_proj_pos.lean:2:18: error: don't know how to synthesize placeholder
context:
h : true ∨ true
⊢ true → true
state:
h : true ∨ true
⊢ true