@[inline]

def Blaster.Optimize.notDecideProp? (op : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op the operand for not,

• When op := decide' e
  • return some decide' (¬ e)
• Otherwise:
  • return none

Equations

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

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

Apply the following simplification/normalization rules on not :

• ! true ==> false
• ! false ==> true
• ! (! e) ==> e
• !(decide' e) ==> decide' (¬ e) Assume that f = Expr.const ``not. An error is triggered if args.size ≠ 1 (i.e., only fully applied not expected at this stage) TODO: consider additional simplification rules

Equations

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

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

Apply simplification/normalization rules on Boolean not operator.

Equations

• Blaster.Optimize.optimizeBoolNot? (Lean.Expr.const `Bool.not us) args = do let a ← Blaster.Optimize.optimizeBoolNot (Lean.Expr.const `Bool.not us) args pure (some a)
• Blaster.Optimize.optimizeBoolNot? f args = pure none