def «term_⇓» : Lean.TrailingParserDescr

A notation for totality of a partial element (we find writing x.Dom a bit silly).

Equations

• «term_⇓» = Lean.ParserDescr.trailingNode `«term_⇓» 50 1024 (Lean.ParserDescr.symbol " ⇓ ")

class HasDot (A : Type u_1) : Type u_1

A generic notation for a left-associative binary operation.

• dot : A → A → A

  (possibly partial) binary application

def «term_⬝_» : Lean.TrailingParserDescr

(possibly partial) binary application

Equations

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

class PartialApplication (A : Type u_1) : Type u_1

A partial binary operation on a set.

• app : Part A → Part A → Part A

  Partial application

instance PartialApplication.hasDot {A : Type u_1} [PartialApplication A] : HasDot (Part A)

Equations

• PartialApplication.hasDot = { dot := PartialApplication.app }