LeanPool.ZFLean.Tactics

Imported Lean Pool material for LeanPool.ZFLean.Tactics.

def Parser.Attr.zrel : Lean.ParserDescr

Imported ZFLean declaration.

Equations

• Parser.Attr.zrel = Lean.ParserDescr.node `Parser.Attr.zrel 1024 (Lean.ParserDescr.nonReservedSymbol "zrel" false)

def Parser.Attr.zpfun : Lean.ParserDescr

Imported ZFLean declaration.

Equations

• Parser.Attr.zpfun = Lean.ParserDescr.node `Parser.Attr.zpfun 1024 (Lean.ParserDescr.nonReservedSymbol "zpfun" false)

def Parser.Attr.zfun : Lean.ParserDescr

Imported ZFLean declaration.

Equations

• Parser.Attr.zfun = Lean.ParserDescr.node `Parser.Attr.zfun 1024 (Lean.ParserDescr.nonReservedSymbol "zfun" false)

Thanks to Ghilain for the idea of registering specific attributes.

def ZFTactics.tacticZrel : Lean.ParserDescr

Imported ZFLean declaration.

Equations

• ZFTactics.tacticZrel = Lean.ParserDescr.node `ZFTactics.tacticZrel 1024 (Lean.ParserDescr.nonReservedSymbol "zrel" false)

def ZFTactics.tacticZpfun : Lean.ParserDescr

Imported ZFLean declaration.

Equations

• ZFTactics.tacticZpfun = Lean.ParserDescr.node `ZFTactics.tacticZpfun 1024 (Lean.ParserDescr.nonReservedSymbol "zpfun" false)

def ZFTactics.tacticZfun : Lean.ParserDescr

Imported ZFLean declaration.

Equations

• ZFTactics.tacticZfun = Lean.ParserDescr.node `ZFTactics.tacticZfun 1024 (Lean.ParserDescr.nonReservedSymbol "zfun" false)