HasCASL/test/Subtype2.hascasl

1
2
3
4
5
6
7
8
9
types S, T
type Binary < S * S -> T
vars a, b: Type; a < b
op   down: b ->? a
var  y: b; x: a
. down y = x

types Nat < Int; Inj < Int -> Int