From 6bdfde7939d57d968c5d00d14a8329d8cd7aa037 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 11 Oct 2023 23:08:46 -0400 Subject: [PATCH] fix: quot reduction bug --- src/kernel/quot.h | 2 +- tests/lean/run/2672.lean | 13 +++++++++++++ 2 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/2672.lean diff --git a/src/kernel/quot.h b/src/kernel/quot.h index 0c47143850..ddfd269ff9 100644 --- a/src/kernel/quot.h +++ b/src/kernel/quot.h @@ -58,7 +58,7 @@ template optional 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]; diff --git a/tests/lean/run/2672.lean b/tests/lean/run/2672.lean new file mode 100644 index 0000000000..5995644624 --- /dev/null +++ b/tests/lean/run/2672.lean @@ -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}