Supplemental notation classes

Heterogeneous notation classes

class FFL.HTilde (α : Type u_1) (β : outParam (Type u_2)) : Type (max u_1 u_2)

• hTilde : α → β

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

Equations

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

class FFL.HArrow (α : Type u_1) (β : Type u_2) (γ : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

• hArrow : α → β → γ

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

Equations

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

class FFL.HWedge (α : Type u_1) (β : Type u_2) (γ : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

• hWedge : α → β → γ

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

Equations

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

class FFL.HVee (α : Type u_1) (β : Type u_2) (γ : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

• hVee : α → β → γ

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

Equations

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

Homogeneous notation classes

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

• tilde : α → α

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

• arrow : α → α → α

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

• wedge : α → α → α

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

• vee : α → α → α

@[instance_reducible, defaultInstance 1000]

instance FFL.Tilde.instHTilde {α : Type u_1} [Tilde α] : HTilde α α

Equations

• FFL.Tilde.instHTilde = { hTilde := FFL.Tilde.tilde }

@[instance_reducible, defaultInstance 1000]

instance FFL.Arrow.instHArrow {α : Type u_1} [Arrow α] : HArrow α α α

Equations

• FFL.Arrow.instHArrow = { hArrow := FFL.Arrow.arrow }

@[instance_reducible, defaultInstance 1000]

instance FFL.Wedge.instHWedge {α : Type u_1} [Wedge α] : HWedge α α α

Equations

• FFL.Wedge.instHWedge = { hWedge := FFL.Wedge.wedge }

@[instance_reducible, defaultInstance 1000]

instance FFL.Vee.instHVee {α : Type u_1} [Vee α] : HVee α α α

Equations

• FFL.Vee.instHVee = { hVee := FFL.Vee.vee }

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

• box : α → α

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

Equations

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

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

• dia : α → α

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

Equations

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

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

• rhd : α → α → α

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

Equations

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

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

• exp : α → α

class FFL.Superexp (α : Type u_1) : Type u_1

• superexp : α → α

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

• smash : α → α → α

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

Equations

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

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

• length : α → α

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

Equations

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

class FFL.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 FFL.«term⌜_⌝» : Lean.ParserDescr

Equations

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

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

• sigma : α

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

• pi : α

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

• delta : α

def FFL.«term𝚺» : Lean.ParserDescr

Equations

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

def FFL.«term𝚷» : Lean.ParserDescr

Equations

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

def FFL.«term𝚫» : Lean.ParserDescr

Equations

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