TypeConstraint

private package

source code: - test_workspace/TypeConstraint.bosatsu

Index

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

references: Eq, Sub

def eq_to_sub[a, b](eq: Eq[a, b]) -> Sub[a, b]

eq_to_sup

references: Eq, 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

references: Sub, 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

references: Sub, Sup

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]