Supplemental notation classes

class LO.Tilde (α : Type u_1) : Type u_1

• tilde : α → α

def LO.«term∼_» : Lean.ParserDescr

Equations

• LO.«term∼_» = Lean.ParserDescr.node `LO.«term∼_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 75))

class LO.Arrow (α : Type u_1) : Type u_1

• arrow : α → α → α

def LO.«term_🡒_» : Lean.TrailingParserDescr

Equations

• LO.«term_🡒_» = Lean.ParserDescr.trailingNode `LO.«term_🡒_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " 🡒 ") (Lean.ParserDescr.cat `term 60))

class LO.Wedge (α : Type u_1) : Type u_1

• wedge : α → α → α

def LO.«term_⋏_» : Lean.TrailingParserDescr

Equations

• LO.«term_⋏_» = Lean.ParserDescr.trailingNode `LO.«term_⋏_» 69 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋏ ") (Lean.ParserDescr.cat `term 69))

class LO.Vee (α : Type u_1) : Type u_1

• vee : α → α → α

def LO.«term_⋎_» : Lean.TrailingParserDescr

Equations

• LO.«term_⋎_» = Lean.ParserDescr.trailingNode `LO.«term_⋎_» 68 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋎ ") (Lean.ParserDescr.cat `term 68))

class LO.Box (α : Type u_1) : Type u_1

• box : α → α

def LO.«term□_» : Lean.ParserDescr

Equations

• LO.«term□_» = Lean.ParserDescr.node `LO.«term□_» 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `term 76))

class LO.Dia (α : Type u_1) : Type u_1

• dia : α → α

def LO.«term◇_» : Lean.ParserDescr

Equations

• LO.«term◇_» = Lean.ParserDescr.node `LO.«term◇_» 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇") (Lean.ParserDescr.cat `term 76))

class LO.Rhd (α : Type u_1) : Type u_1

• rhd : α → α → α

def LO.«term_▷_» : Lean.TrailingParserDescr

Equations

• LO.«term_▷_» = Lean.ParserDescr.trailingNode `LO.«term_▷_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ▷ ") (Lean.ParserDescr.cat `term 71))

class LO.Tensor (α : Type u_1) : Type u_1

• tensor : α → α → α

def LO.«term_⨂_» : Lean.TrailingParserDescr

Equations

• LO.«term_⨂_» = Lean.ParserDescr.trailingNode `LO.«term_⨂_» 69 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨂ ") (Lean.ParserDescr.cat `term 69))

class LO.Par (α : Type u_1) : Type u_1

• par : α → α → α

def LO.term_⅋_ : Lean.TrailingParserDescr

Equations

• LO.term_⅋_ = Lean.ParserDescr.trailingNode `LO.term_⅋_ 68 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⅋ ") (Lean.ParserDescr.cat `term 68))

class LO.With (α : Type u_1) : Type u_1

• with' : α → α → α

def LO.«term_＆_» : Lean.TrailingParserDescr

Note that this notation "＆" (U+FF06) is distinct from "&" (U+0026)

Equations

• LO.«term_＆_» = Lean.ParserDescr.trailingNode `LO.«term_＆_» 69 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ＆ ") (Lean.ParserDescr.cat `term 69))

class LO.Plus (α : Type u_1) : Type u_1

• plus : α → α → α

def LO.«term_⨁_» : Lean.TrailingParserDescr

Equations

• LO.«term_⨁_» = Lean.ParserDescr.trailingNode `LO.«term_⨁_» 68 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨁ ") (Lean.ParserDescr.cat `term 68))

class LO.Lolli (α : Type u_1) : Type u_1

• lolli : α → α → α

def LO.«term_⊸_» : Lean.TrailingParserDescr

Equations

• LO.«term_⊸_» = Lean.ParserDescr.trailingNode `LO.«term_⊸_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊸ ") (Lean.ParserDescr.cat `term 60))

class LO.Bang (α : Type u_1) : Type u_1

• bang : α → α

def LO.«term！_» : Lean.ParserDescr

Note that this notation "！" (U+FF01) is distinct from "!" (U+0021)

Equations

• LO.«term！_» = Lean.ParserDescr.node `LO.«term！_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "！") (Lean.ParserDescr.cat `term 75))

class LO.Quest (α : Type u_1) : Type u_1

• quest : α → α

def LO.«term？_» : Lean.ParserDescr

Notice that this notation "？" (U+FF1F) is distinct from "?" (U+003F)

Equations

• LO.«term？_» = Lean.ParserDescr.node `LO.«term？_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "？") (Lean.ParserDescr.cat `term 75))

class LO.Exp (α : Type u_1) : Type u_1

• exp : α → α

class LO.Smash (α : Type u_1) : Type u_1

• smash : α → α → α

def LO.«term_⨳_» : Lean.TrailingParserDescr

Equations

• LO.«term_⨳_» = Lean.ParserDescr.trailingNode `LO.«term_⨳_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨳ ") (Lean.ParserDescr.cat `term 81))

class LO.Length (α : Type u_1) : Type u_1

• length : α → α

def LO.«term‖_‖» : Lean.ParserDescr

Equations

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

class LO.GödelQuote (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)

Coding objects into syntactic objects (e.g. natural numbers, first-order terms)

• quote : α → β

def LO.«term⌜_⌝» : Lean.ParserDescr

Equations

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

class LO.SigmaSymbol (α : Type u_1) : Type u_1

• sigma : α

class LO.PiSymbol (α : Type u_1) : Type u_1

• pi : α

class LO.DeltaSymbol (α : Type u_1) : Type u_1

• delta : α

def LO.«term𝚺» : Lean.ParserDescr

Equations

• LO.«term𝚺» = Lean.ParserDescr.node `LO.«term𝚺» 1024 (Lean.ParserDescr.symbol "𝚺")

def LO.«term𝚷» : Lean.ParserDescr

Equations

• LO.«term𝚷» = Lean.ParserDescr.node `LO.«term𝚷» 1024 (Lean.ParserDescr.symbol "𝚷")

def LO.«term𝚫» : Lean.ParserDescr

Equations

• LO.«term𝚫» = Lean.ParserDescr.node `LO.«term𝚫» 1024 (Lean.ParserDescr.symbol "𝚫")