def Blaster.Optimize.optimizeDecideCore (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Apply the following simplification/normalization rules on Blaster.decide':

• decide' False ==> false
• decide' True ==> true
• decide' (true = p) ==> p
• decide' (false = p) ==> ! p An error is trigerred if args.size ≠ 2.

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Optimize.optimizeDecideCore.decideBoolEq? (e : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Return some p if e := true = p Return some (! p) if e := false = p Otherwise none.

Equations

• One or more equations did not get rendered due to their size.

def Blaster.Optimize.optimizeDecide? (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Apply simplification/normalization rules on Blaster.decide'.

Equations

• Blaster.Optimize.optimizeDecide? (Lean.Expr.const `Blaster.decide' us) args = do let a ← Blaster.Optimize.optimizeDecideCore (Lean.Expr.const `Blaster.decide' us) args pure (some a)
• Blaster.Optimize.optimizeDecide? f args = pure none