Notation and core classes for partial combinatory algebras

A notation for totality of a partial element, a generic class for a left-associative binary application operator, and the class for a partial binary operation on a type.

def LeanPool.PartialCombinatoryAlgebras.«term_⇓» : Lean.TrailingParserDescr

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

Equations

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

class LeanPool.PartialCombinatoryAlgebras.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 LeanPool.PartialCombinatoryAlgebras.«term_⬝_» : Lean.TrailingParserDescr

(possibly partial) binary application

Equations

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

class LeanPool.PartialCombinatoryAlgebras.PartialApplication (A : Type u_1) : Type u_1

A partial binary operation on a set.

• app : Part A → Part A → Part A

  Partial application

@[implicit_reducible]

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

Equations

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