def Aesop.RuleBuilderOptions.forwardTransparency (opts : Aesop.RuleBuilderOptions) : Lean.Meta.TransparencyMode

Equations

• Aesop.RuleBuilderOptions.forwardTransparency opts = Option.getD opts.transparency? Lean.Meta.TransparencyMode.default

def Aesop.RuleBuilderOptions.forwardIndexTransparency (opts : Aesop.RuleBuilderOptions) : Lean.Meta.TransparencyMode

Equations

• Aesop.RuleBuilderOptions.forwardIndexTransparency opts = Option.getD opts.indexTransparency? Lean.Meta.TransparencyMode.reducible

def Aesop.RuleBuilderOptions.forwardIndexingMode (type : Lean.Expr) (immediate : Aesop.UnorderedArraySet Nat) (opts : Aesop.RuleBuilderOptions) : Lean.MetaM Aesop.IndexingMode

Equations

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

def Aesop.RuleBuilder.getImmediatePremises (stx : Lean.Term) (type : Lean.Expr) (pat? : Option Aesop.RulePattern) (md : Lean.Meta.TransparencyMode) : Option (Array Lean.Name) → Lean.MetaM (Aesop.UnorderedArraySet Nat)

Equations

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

def Aesop.RuleBuilder.getImmediatePremises.isPatternInstantiated (pat? : Option Aesop.RulePattern) (i : Nat) : Bool

Equations

• Aesop.RuleBuilder.getImmediatePremises.isPatternInstantiated pat? i = let idx? := do let __do_lift ← pat? let __do_lift ← __do_lift.argMap[i]? __do_lift; Option.isSome idx?

def Aesop.RuleBuilder.getImmediatePremises.errPrefix (stx : Lean.Term) : Lean.MessageData

Equations

• Aesop.RuleBuilder.getImmediatePremises.errPrefix stx = Lean.toMessageData "aesop: while registering '" ++ Lean.toMessageData stx ++ Lean.toMessageData "' as a forward rule"

def Aesop.RuleBuilder.forwardCore (isDestruct : Bool) : Aesop.RuleBuilder

Equations

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

def Aesop.RuleBuilder.forward : Aesop.RuleBuilder

Equations

• Aesop.RuleBuilder.forward = Aesop.RuleBuilder.forwardCore false

def Aesop.RuleBuilder.destruct : Aesop.RuleBuilder

Equations

• Aesop.RuleBuilder.destruct = Aesop.RuleBuilder.forwardCore true