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

Equations

• opts.forwardTransparency = opts.transparency?.getD Lean.Meta.TransparencyMode.reducible

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

Equations

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

def Aesop.RuleBuilder.getForwardIndexingMode (type : Lean.Expr) (immediate : UnorderedArraySet PremiseIndex) : Lean.MetaM IndexingMode

Equations

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

def Aesop.RuleBuilder.getImmediatePremises (type : Lean.Expr) (pat? : Option RulePattern) : Option (Array Lean.Name) → Lean.MetaM (UnorderedArraySet PremiseIndex)

Equations

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

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

Equations

• Aesop.RuleBuilder.getImmediatePremises.isPatternInstantiated pat? i = (do let __do_lift ← pat? let __do_lift ← __do_lift.argMap[i]? __do_lift).isSome

def Aesop.RuleBuilder.getImmediatePremises.errPrefix : Lean.MessageData

Equations

• Aesop.RuleBuilder.getImmediatePremises.errPrefix = Lean.toMessageData "aesop: forward builder: "

def Aesop.RuleBuilder.forwardCore₂ (t : ElabRuleTerm) (immediate? : Option (Array Lean.Name)) (pat? : Option RulePattern) (phase : PhaseSpec) (isDestruct : Bool) : Lean.MetaM ForwardRule

Equations

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

def Aesop.RuleBuilder.forwardCore (t : ElabRuleTerm) (immediate? : Option (Array Lean.Name)) (pat? : Option RulePattern) (phase : PhaseSpec) (isDestruct : Bool) : Lean.MetaM LocalRuleSetMember

Equations

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

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

Equations

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