diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean index 3206481113..388ae6f195 100644 --- a/src/Lean/Compiler/ConstFolding.lean +++ b/src/Lean/Compiler/ConstFolding.lean @@ -150,36 +150,8 @@ def natFoldFns : List (Name × BinFoldFn) := (``Nat.ble, foldNatBle) ] -def getBoolLit : Expr → Option Bool - | Expr.const ``Bool.true _ => some true - | Expr.const ``Bool.false _ => some false - | _ => none - -def foldStrictAnd (_ : Bool) (a₁ a₂ : Expr) : Option Expr := - let v₁ := getBoolLit a₁ - let v₂ := getBoolLit a₂ - match v₁, v₂ with - | some true, _ => a₂ - | some false, _ => a₁ - | _, some true => a₁ - | _, some false => a₂ - | _, _ => none - -def foldStrictOr (_ : Bool) (a₁ a₂ : Expr) : Option Expr := - let v₁ := getBoolLit a₁ - let v₂ := getBoolLit a₂ - match v₁, v₂ with - | some true, _ => a₁ - | some false, _ => a₂ - | _, some true => a₂ - | _, some false => a₁ - | _, _ => none - -def boolFoldFns : List (Name × BinFoldFn) := - [(``strictOr, foldStrictOr), (``strictAnd, foldStrictAnd)] - def binFoldFns : List (Name × BinFoldFn) := - boolFoldFns ++ uintBinFoldFns ++ natFoldFns + uintBinFoldFns ++ natFoldFns def foldNatSucc (_ : Bool) (a : Expr) : Option Expr := do let n ← getNumLit a diff --git a/tests/compiler/strictOrSimp.lean b/tests/compiler/strictOrSimp.lean deleted file mode 100644 index ea135c5015..0000000000 --- a/tests/compiler/strictOrSimp.lean +++ /dev/null @@ -1,11 +0,0 @@ -partial def spin : Nat → Bool -| n => spin (n) - -@[inline] def C : Nat := 0 - -def f (b : Nat) := -if strictOr (C == 0) (spin b) then "hello" -else "world" - -def main (xs : List String) : IO Unit := -IO.println (f 0)