The primrec tactic

Proves Primrec f by reading the shape of f off the goal, via Aesop. The rules are in Foundation/Vorspiel/Computability/Primrec.lean; @[primrec] adds more.

def primrecConfig : Aesop.Options

Equations

• primrecConfig = { maxRuleApplicationDepth := 100, maxRuleApplications := 4000, terminal := true, useSimpAll := false, useDefaultSimpSet := false }

def attrPrimrec : Lean.ParserDescr

Adds a lemma of the form Primrec fun a ↦ F (f a) (g a) to the primrec rule set.

Equations

• attrPrimrec = Lean.ParserDescr.node `attrPrimrec 1024 (Lean.ParserDescr.nonReservedSymbol "primrec" false)

def tacticPrimrec_ : Lean.ParserDescr

Proves Primrec f, Primrec₂ f, PrimrecPred p or PrimrecRel r.

Equations

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

def tacticPrimrec?_ : Lean.ParserDescr

Equations

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