Hypercube/Tst.hs at master · reflectionalist/Hypercube · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
import Prelude hiding (all)
import UTT


tm1  = all ("x", typ 0) (var "x")
tps1 = [ all ("x", typ 0) (typ 0)
       , typ 0 ]

tm2  = als [("x", typ 0), ("y", typ 0)] (var "y")
tps2 = [ als [("x", typ 0), ("y", typ 0)] (typ 0)
       , all ("x", typ 0) (typ 0)
       , typ 0 ]

tm3  = als [ ("x1", typ 0), ("x2", all ("y", nat) (typ 0))
           , ("x3", nat), ("x4", app (var "x2") (var "x3")) ]
           (app (var "x2") (var "x3"))
tps3 = [ als [ ("x1", typ 0), ("x2", all ("y", nat) (typ 0))
             , ("x3", nat), ("x4", app (var "x2") (var "x3")) ]
             (typ 0)
       , als [("x1", typ 0), ("x2", all ("y", nat) (typ 0)), ("x3", nat)] (typ 0)
       , als [("x1", typ 0), ("x2", all ("y", nat) (typ 0))] (typ 0)
       , all ("x1", typ 0) (typ 0)
       , typ 0 ]

id1 = als [("X", typ 0), ("x", var "X")] (var "x")

bi2 = bin ("X", typ 0, nat) (all ("x", var "X") (var "x"))