Rule set for Complexitylib's polynomial-time certificates

def Complexity.attrPolytime : Lean.ParserDescr

Register a proved closure rule or algorithm certificate for polytime. Unindexed matching also finds a closure rule when its input function simplifies to identity.

Equations

• Complexity.attrPolytime = Lean.ParserDescr.node `Complexity.attrPolytime 1024 (Lean.ParserDescr.nonReservedSymbol "polytime" false)