sample.itt

def Era = {10 x x}
def Unit.new = (x x)
def Unit.id = ((x x) (y y))
def Bool.true = ((a a) (b b))
def Bool.false = ((a b) (a b))

def Bool.id = (x x)
def Bool.not = (((a b) (c d)) ((d b) (c a)))


def Ann = ([a b] (<b c> [a c]))
def Check = ([b a] (<b c> [c a]))
def Bool = <((a b) (c d)) ((d c) (b a))>
def Unit = <(x x) (y y)>

def Arrow = term λAλBθfλx<(f <x: A>): B>
def RestrictDomain = term λfλAλx(f <x: A>)

def test goodtest_1 = term λx (Check (Bool.not (Ann x Bool)) Bool)
def test goodtest_2 = term λx (Check (Unit.id (Ann x Unit)) Unit)
def test goodtest_3 = term (Check Unit.new Unit)
def test goodtest_4 = term (Check Bool.false Unit)
def test goodtest_5 = term (Check Unit.new Bool)
def test goodtest_6 = term (Check λx(Bool.id (Bool.not x)) (Arrow Bool Bool))
def test goodtest_7 = term (Check λx(Bool.id (Bool.id x)) (Arrow Bool Bool))
def test goodtest_8 = term (Check Bool.false Bool)
def test goodtest_9 = term (Check λx<x: Unit> (Arrow Unit Unit))
def test goodtest_10 = term (Check (RestrictDomain λx x Unit) (Arrow Unit Unit))
def test goodtest_11 = term (Check (RestrictDomain λx (x Bool.true) Unit) (Arrow Unit Bool))
def test goodtest_12 = term (Check (RestrictDomain Bool.not Unit) (Arrow Unit Bool))

def test badtest_1 = term (Check Bool.true Unit)
def test badtest_2 = term (Check Ann Bool)
def test badtest_3 = term (Check (RestrictDomain λx<(Bool.not x): Bool> Bool) (Arrow Bool Unit))

term λx x