TypeConstraint

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

def cast[a, b](s: Eq[a, b], a: a) -> b

compose_eq

def compose_eq[a, b, c](first: Eq[a, b], second: Eq[b, c]) -> Eq[a, c]

compose_sub

def compose_sub[a, b, c](first: Sub[a, b], second: Sub[b, c]) -> Sub[a, c]

compose_sup

def compose_sup[a, b, c](first: Sup[a, b], second: Sup[b, c]) -> Sup[a, c]

downcast

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

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

narrow

def narrow[a, b, c: -* -> *](s: Sup[a, b], fa: c[a]) -> c[b]

refl

refl: forall a: *. Eq[a, a]

refl_sub

refl_sub: forall a: *. Sub[a, a]

refl_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

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

def upcast[a, b](s: Sub[a, b], a: a) -> b

widen

def widen[a, b, c: +* -> *](s: Sub[a, b], fa: c[a]) -> c[b]