def TLA.Expr.splitAndIntoParts (p : Lean.Expr) : Lean.MetaM (List Lean.Expr)

Split a TLA conjunction Expr into its list of conjuncts.

Equations

• TLA.Expr.splitAndIntoParts ((((Lean.Expr.const `TLA.tlaAnd us).app arg).app a).app b) = do let as ← TLA.Expr.splitAndIntoParts a let bs ← TLA.Expr.splitAndIntoParts b pure (as ++ bs)
• TLA.Expr.splitAndIntoParts p = pure [p]

def TLA.Expr.splitImplicationsIntoParts (p : Lean.Expr) (cutAnd? : Bool := true) : Lean.MetaM (List Lean.Expr × Lean.Expr)

Split a chain of TLA implications into its list of premises and conclusion, optionally further splitting each premise conjunction (cutAnd?).

Equations

• One or more equations did not get rendered due to their size.
• TLA.Expr.splitImplicationsIntoParts p cutAnd? = pure ([], p)

def TLA.Expr.splitPredImpliesIntoParts (p : Lean.Expr) : Lean.MetaM (List Lean.Expr × Lean.Expr)

Split a predImplies/valid statement into its premises and conclusion.

Equations

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

def TLA.Expr.peekStateType (p : Lean.Expr) : Option Lean.Expr

Given some TLA related expression and return the type of the state (i.e., the argument after TLA.pred). While this could be done via inferType, just peeking the expression should be much "cheaper".

Equations

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