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

Apply the following COI reduction rule on Exists.

• ∃ (n : t), e ===> e (if isSortOrInhabited t ∧ ¬ e.hasLooseBVar e 0). Note that ∃ (n : t), e is internally represented as app (app Exists t) (lam n t e _). Assmes that f := Expr.const ``Exists An error is trigerred if args.size ≠ 2.

Equations

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

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

Apply simplification/normalization rules on Exists.

Equations

• Blaster.Optimize.optimizeExists? (Lean.Expr.const `Exists us) args = do let a ← Blaster.Optimize.coiExists (Lean.Expr.const `Exists us) args pure (some a)
• Blaster.Optimize.optimizeExists? f args = pure none