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

fix(frontends/lean): closes #1898

Browse source
This commit is contained in:
Leonardo de Moura 2018-01-02 12:27:39 -08:00
parent acf4b56cd4
commit 8621be6335
5 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1061,10 +1061,7 @@ parse_table init_nud_table() {
static expr parse_field(parser_state & p, unsigned, expr const * args, pos_info const & pos) {
try {
if (p.curr_is_numeral()) {
pos_info num_pos = p.pos();
unsigned fidx = p.parse_small_nat();
if (fidx == 0)
return p.parser_error_or_expr({"invalid projection, index must be greater than 0", num_pos});
return p.save_pos(mk_field_notation(args[0], fidx), pos);
} else {
name field = p.check_id_next("identifier or numeral expected");

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

@ -2784,7 +2784,9 @@ elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr cons
}
auto fnames = get_structure_fields(m_env, const_name(I));
unsigned fidx = get_field_notation_field_idx(e);
lean_assert(fidx > 0);
if (fidx == 0) {
throw elaborator_exception(e, "invalid projection, index must be greater than 0");
}
if (fidx > fnames.size()) {
auto pp_fn = mk_pp_ctx();
throw elaborator_exception(e, format("invalid projection, structure has only ") +

1
tests/lean/1898.lean Normal file
View file

@ -0,0 +1 @@
def X (R : Type) [H : comm_ring R] := H.0

6
tests/lean/1898.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
1898.lean:1:39: error: invalid projection, index must be greater than 0
1898.lean:1:4: error: don't know how to synthesize placeholder
context:
R : Type,
H : comm_ring R
⊢ Sort ?

2
tests/lean/proj_notation.lean.expected.out
View file

@ -10,7 +10,7 @@ proj_notation.lean:29:19: error: invalid field notation, 'fst' is not a valid "f
which has type
car
λ (c : car), ⁇ : car → ?M_1
proj_notation.lean:31:21: error: invalid projection, index must be greater than 0
proj_notation.lean:31:19: error: invalid projection, index must be greater than 0
λ (c : car), ⁇ : car → ?M_1
proj_notation.lean:33:19: error: invalid projection, structure has only 2 field(s)
c