Custom tactics for ZF

This file registers label attributes and defines the zrel, zpfun, zfun, and zdom tactics used to discharge relation, partial-function, function, and domain-membership side goals.

def Parser.Attr.zrel : Lean.ParserDescr

Equations

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

def Parser.Attr.zpfun : Lean.ParserDescr

Equations

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

def Parser.Attr.zfun : Lean.ParserDescr

Equations

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

def Parser.Attr.zdom : Lean.ParserDescr

Equations

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

def Parser.Attr.zdom_conv : Lean.ParserDescr

Equations

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

Thanks to Ghilain for the idea of registering specific attributes

def ZFTactics.tacticZrel : Lean.ParserDescr

Equations

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

def ZFTactics.tacticZpfun : Lean.ParserDescr

Equations

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

def ZFTactics.tacticZfun : Lean.ParserDescr

Equations

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

def ZFTactics.tacticZdom : Lean.ParserDescr

Equations

• ZFTactics.tacticZdom = Lean.ParserDescr.node `ZFTactics.tacticZdom 1024 (Lean.ParserDescr.nonReservedSymbol "zdom" false)