From a6ba7312cc7c8a95b258353325d34ff36b24babe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Tue, 10 Feb 2026 19:02:01 +0000 Subject: [PATCH] chore: make `toBetaApp` public (#12416) This PR makes `Sym.Simp.toBetaApp` public. This is necessary for the refactor of the main `cbv` simproc in #12417. --- src/Lean/Meta/Sym/Simp/Have.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Sym/Simp/Have.lean b/src/Lean/Meta/Sym/Simp/Have.lean index 95a3a61de9..76740eb876 100644 --- a/src/Lean/Meta/Sym/Simp/Have.lean +++ b/src/Lean/Meta/Sym/Simp/Have.lean @@ -84,7 +84,7 @@ We produce: where each `xᵢ'` has type `deps_type → Tᵢ` and `b'` contains applications `xᵢ' (deps)`. -/ -structure ToBetaAppResult where +public structure ToBetaAppResult where /-- Type of the input `have`-expression. -/ α : Expr /-- The universe level of `α`. -/ @@ -147,7 +147,7 @@ For each `have xᵢ := vᵢ` where `vᵢ` depends on `xᵢ₁, ..., xᵢₖ` (ak The proof is `rfl` since the transformation is definitionally equal. -/ -def toBetaApp (haveExpr : Expr) : SymM ToBetaAppResult := do +public def toBetaApp (haveExpr : Expr) : SymM ToBetaAppResult := do go haveExpr #[] #[] #[] #[] #[] #[] {} where /--