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

chore: make simpCond public (#12391)

Browse source 
This PR makes `simpCond` public. It is needed to avoid code duplication
in #12361
This commit is contained in:
Wojciech Różowski 2026-02-09 13:54:36 +00:00 • committed by GitHub
parent 7a8e011603
commit 4401117a6a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Sym/Simp/ControlFlow.lean
View file

@ -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