def Iris.ProofMode.icasesPat.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.icasesPat : Category

Equations

• Lean.Parser.Category.icasesPat = { }

def Iris.ProofMode.icasesPatAlts : Lean.ParserDescr

Equations

• Iris.ProofMode.icasesPatAlts = Lean.ParserDescr.nodeWithAntiquot "icasesPatAlts" `Iris.ProofMode.icasesPatAlts ((Lean.ParserDescr.cat `icasesPat 0).sepBy1 " | " (Lean.ParserDescr.symbol " | "))

def Iris.ProofMode.icasesPat_ : Lean.ParserDescr

Equations

• Iris.ProofMode.icasesPat_ = Lean.ParserDescr.node `Iris.ProofMode.icasesPat_ 1022 Lean.binderIdent

def Iris.ProofMode.«icasesPat-» : Lean.ParserDescr

Equations

• Iris.ProofMode.«icasesPat-» = Lean.ParserDescr.node `Iris.ProofMode.«icasesPat-» 1024 (Lean.ParserDescr.symbol "-")

def Iris.ProofMode.«icasesPat⟨_⟩» : Lean.ParserDescr

Equations

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

def Iris.ProofMode.«icasesPat(_)» : Lean.ParserDescr

Equations

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

def Iris.ProofMode.«icasesPat⌜_⌝» : Lean.ParserDescr

Equations

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

def Iris.ProofMode.«icasesPat□_» : Lean.ParserDescr

Equations

• Iris.ProofMode.«icasesPat□_» = Lean.ParserDescr.node `Iris.ProofMode.«icasesPat□_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `icasesPat 0))

def Iris.ProofMode.«icasesPat∗_» : Lean.ParserDescr

Equations

• Iris.ProofMode.«icasesPat∗_» = Lean.ParserDescr.node `Iris.ProofMode.«icasesPat∗_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∗") (Lean.ParserDescr.cat `icasesPat 0))

def Iris.ProofMode.«icasesPat%_» : Lean.ParserDescr

Equations

• Iris.ProofMode.«icasesPat%_» = Lean.ParserDescr.node `Iris.ProofMode.«icasesPat%_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "%") (Lean.ParserDescr.cat `icasesPat 0))

def Iris.ProofMode.«icasesPat#_» : Lean.ParserDescr

Equations

• Iris.ProofMode.«icasesPat#_» = Lean.ParserDescr.node `Iris.ProofMode.«icasesPat#_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `icasesPat 0))

def Iris.ProofMode.«icasesPat*_» : Lean.ParserDescr

Equations

• Iris.ProofMode.«icasesPat*_» = Lean.ParserDescr.node `Iris.ProofMode.«icasesPat*_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*") (Lean.ParserDescr.cat `icasesPat 0))

inductive Iris.ProofMode.iCasesPat : Type

• one (name : Lean.TSyntax `Lean.binderIdent) : iCasesPat
• clear : iCasesPat
• conjunction (args : List iCasesPat) : iCasesPat
• disjunction (args : List iCasesPat) : iCasesPat
• pure (pat : iCasesPat) : iCasesPat
• intuitionistic (pat : iCasesPat) : iCasesPat
• spatial (pat : iCasesPat) : iCasesPat

instance Iris.ProofMode.instReprICasesPat : Repr iCasesPat

Equations

• Iris.ProofMode.instReprICasesPat = { reprPrec := Iris.ProofMode.repriCasesPat✝ }

instance Iris.ProofMode.instInhabitedICasesPat : Inhabited iCasesPat

Equations

• Iris.ProofMode.instInhabitedICasesPat = { default := Iris.ProofMode.iCasesPat.one default }

def Iris.ProofMode.iCasesPat.parse (pat : Lean.TSyntax `icasesPat) : Lean.MacroM iCasesPat

Equations

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

partial def Iris.ProofMode.iCasesPat.parse.go : Lean.TSyntax `icasesPat → Option iCasesPat

partial def Iris.ProofMode.iCasesPat.parse.goAlts : Lean.TSyntax `Iris.ProofMode.icasesPatAlts → Option iCasesPat