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

fix: quot reduction bug

Browse source
This commit is contained in:
Mario Carneiro 2023-10-11 23:08:46 -04:00 • committed by Leonardo de Moura
parent 5d096c3fd8
commit 6bdfde7939
2 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/quot.h
View file

@ -58,7 +58,7 @@ template<typename WHNF> optional<expr> quot_reduce_rec(expr const & e, WHNF cons
expr mk = whnf(args[mk_pos]);
expr const & mk_fn = get_app_fn(mk);
if (!is_constant(mk_fn) || const_name(mk_fn) != *quot_consts::g_quot_mk)
if (!is_constant(mk_fn) || const_name(mk_fn) != *quot_consts::g_quot_mk || get_app_num_args(mk) != 3)
return none_expr();
expr const & f = args[arg_pos];

13
tests/lean/run/2672.lean Normal file
View file

@ -0,0 +1,13 @@
import Lean
open Lean Elab Term
elab "foo" t:term "," s:term : term => do
let e ← Elab.Term.elabTermAndSynthesize t none
let e2 ← Elab.Term.elabTermAndSynthesize s none
let t ← ofExceptKernelException (Kernel.whnf (← getEnv) (← getLCtx) (.app e e2))
println! t
return e
variable {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β)
(H : ∀ (a b : α), r a b → f a = f b)
example := foo @Quot.lift.{u, v} α r β f H, @Quot.mk.{u}