TypeConstraint
private package
source code: - test_workspace/TypeConstraint.bosatsu
Index
- Types:
Eq,Sub,Sup - Values:
cast,compose_eq,compose_sub,compose_sup,downcast,eq_to_sub,eq_to_sup,flip_eq,narrow,refl,refl_sub,refl_sup,sub_to_sup,substitute,sup_to_sub,upcast,widen
Types
Eq[a, b]
type Eq[a: *, b: *]
Sub[a, b]
type Sub[a: -*, b: +*]
Sup[a, b]
type Sup[a: +*, b: -*]
Values
cast
references: Eq
def cast[a, b](s: Eq[a, b], a: a) -> b
compose_eq
references: Eq
def compose_eq[a, b, c](first: Eq[a, b], second: Eq[b, c]) -> Eq[a, c]
compose_sub
references: Sub
def compose_sub[a, b, c](first: Sub[a, b], second: Sub[b, c]) -> Sub[a, c]
compose_sup
references: Sup
def compose_sup[a, b, c](first: Sup[a, b], second: Sup[b, c]) -> Sup[a, c]
downcast
references: Sup
def downcast[a, b](s: Sup[a, b], a: b) -> a
eq_to_sub
def eq_to_sub[a, b](eq: Eq[a, b]) -> Sub[a, b]
eq_to_sup
def eq_to_sup[a, b](eq: Eq[a, b]) -> Sup[a, b]
flip_eq
references: Eq
def flip_eq[a, b](eq: Eq[a, b]) -> Eq[b, a]
narrow
references: Sup
def narrow[a, b, c: -* -> *](s: Sup[a, b], fa: c[a]) -> c[b]
refl
references: Eq
refl: forall a: *. Eq[a, a]
refl_sub
references: Sub
refl_sub: forall a: *. Sub[a, a]
refl_sup
references: Sup
refl_sup: forall a: *. Sup[a, a]
sub_to_sup
def sub_to_sup[a, b](sub: Sub[a, b]) -> Sup[b, a]
substitute
references: Eq
def substitute[a, b, c: * -> *](eq: Eq[a, b], fa: c[a]) -> c[b]
sup_to_sub
def sup_to_sub[a, b](sup: Sup[a, b]) -> Sub[b, a]
upcast
references: Sub
def upcast[a, b](s: Sub[a, b], a: a) -> b
widen
references: Sub
def widen[a, b, c: +* -> *](s: Sub[a, b], fa: c[a]) -> c[b]