From 4401117a6a8ebb5f544f1cb176499d7fdc063703 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Mon, 9 Feb 2026 13:54:36 +0000 Subject: [PATCH] chore: make `simpCond` public (#12391) This PR makes `simpCond` public. It is needed to avoid code duplication in #12361 --- src/Lean/Meta/Sym/Simp/ControlFlow.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Sym/Simp/ControlFlow.lean b/src/Lean/Meta/Sym/Simp/ControlFlow.lean index 73da7bd3d7..3acad97ffc 100644 --- a/src/Lean/Meta/Sym/Simp/ControlFlow.lean +++ b/src/Lean/Meta/Sym/Simp/ControlFlow.lean @@ -85,7 +85,7 @@ def simpDIte : Simproc := fun e => do /-- Simplifies a `cond` expression (aka Boolean `if-then-else`). -/ -def simpCond : Simproc := fun e => do +public def simpCond : Simproc := fun e => do let numArgs := e.getAppNumArgs if numArgs < 4 then return .rfl (done := true) propagateOverApplied e (numArgs - 4) fun e => do