class Cslib.HasHContext (α : Type u_1) (β : Type u_2) : Type (max (max u_1 u_2) (u_3 + 1))

Class for types with a canonical notion of heterogeneous single-hole contexts.

• Context : Type u_3

  The type of contexts.

• fill (c : Context α β) (b : β) : α

  Replaces the hole in the context with a value, resulting in a new value.

def Cslib.«term_<[_]» : Lean.TrailingParserDescr

Replaces the hole in the context with a value, resulting in a new value.

Equations

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

@[reducible, inline]

abbrev Cslib.HasContext (α : Type u_1) : Type (max u_1 (u_2 + 1))

Class for types (α) that have a canonical notion of homogeneous single-hole contexts (Context).

Equations

• Cslib.HasContext α = Cslib.HasHContext α α

def Cslib.HasContext.Context (α : Type u_1) [HasContext α] : Type u_2

The type of contexts.

Equations

• Cslib.HasContext.Context α = Cslib.HasHContext.Context α α