fix(kernel/quotient/quotient): bug in reduction rule

This commit is contained in:
Leonardo de Moura 2015-04-29 09:55:14 -07:00
parent d2c7b5c319
commit 051615712c
3 changed files with 14 additions and 0 deletions

View file

@ -82,6 +82,9 @@ optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(e
expr const & f = args[mk_pos-2];
expr r = mk_app(f, app_arg(mk));
unsigned elim_arity = mk_pos+1;
if (args.size() > elim_arity)
r = mk_app(r, args.size() - elim_arity, args.begin() + elim_arity);
return some_ecs(r, mk_cs.second);
}

9
tests/lean/quot_bug.lean Normal file
View file

@ -0,0 +1,9 @@
open quot
variables {A : Type} {B : A → Type}
variable f : Π a : A, B a
eval λ x, quot.lift_on ⟦f⟧ (λf : (Πx : A, B x), f) _ x
example (x : A) : quot.lift_on ⟦f⟧ (λf : (Πx : A, B x), f) sorry x = f x :=
rfl

View file

@ -0,0 +1,2 @@
λ (x : A), f x
quot_bug.lean:8:59: warning: using 'sorry'