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

fix(library/user_recursors): memory access violation

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-19 11:07:31 -07:00
parent 4f12409c63
commit 6da2ba331f
3 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/user_recursors.cpp
View file

@ -100,6 +100,10 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
dep_elim = true;
else
dep_elim = false;
} else if (C_args.empty()) {
throw exception(sstream() << "invalid user defined recursor, '" << r << "' does not support dependent elimination, "
<< "and position of the major premise was not specified "
<< "(solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)");
} else {
major = C_args.back();
dep_elim = true;

4
tests/lean/user_rec_crash.lean Normal file
View file

@ -0,0 +1,4 @@
example (a b : Prop) (h : a ∧ b) : a :=
begin
induction h using and.rec_on with h₁ h₂,
end

14
tests/lean/user_rec_crash.lean.expected.out Normal file
View file

@ -0,0 +1,14 @@
induction: h and.rec_on (h₁ h₂)
user_rec_crash.lean:3:2: error:invalid 'induction' tactic, invalid user defined recursor, 'and.rec_on' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)
proof state:
a b : Prop,
h : a ∧ b
⊢ a
user_rec_crash.lean:4:0: error: don't know how to synthesize placeholder
a b : Prop,
h : a ∧ b
⊢ a
user_rec_crash.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : Prop) (h : …),
?M_1