From 7d1b72da2663aca4e6cf88f2f865846164d22f74 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 17 Mar 2026 17:17:14 +0000 Subject: [PATCH] refactor: use the full features of mkAppM in `free_union` --- Cslib/Foundations/Data/HasFresh.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Cslib/Foundations/Data/HasFresh.lean b/Cslib/Foundations/Data/HasFresh.lean index 9ee2c84c7..691f8afa0 100644 --- a/Cslib/Foundations/Data/HasFresh.lean +++ b/Cslib/Foundations/Data/HasFresh.lean @@ -108,11 +108,12 @@ def HasFresh.freeUnion : TermElab := fun stx _ => do for ldecl in ← getLCtx do if !ldecl.isImplementationDetail then - let local_type ← ldecl.toExpr |> inferType >=> whnf for map in maps do - if let Expr.forallE _ dom _ _ := ← inferType map then - if ← isDefEq local_type dom then - finsets := finsets.push (map.betaRev #[ldecl.toExpr]) + let finset ← try + mkAppM' map #[ldecl.toExpr] + catch _ => + continue + finsets := finsets.push finset.headBeta let _dec : Q(DecidableEq $α) ← synthInstanceQ q(DecidableEq $α) let union := finsets.foldl (fun a b : Q(Finset $α) => q($a ∪ $b)) q(∅)