forked from luoruixuan/prfact
-
Notifications
You must be signed in to change notification settings - Fork 0
/
test.f
49 lines (26 loc) · 737 Bytes
/
test.f
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
/* Examples for testing */
lambda x:Bot. x;
lambda x:Bot. x x;
lambda x:<a:Bool,b:Bool>. x;
lambda x:Top. x;
(lambda x:Top. x) (lambda x:Top. x);
(lambda x:Top->Top. x) (lambda x:Top. x);
(lambda r:{x:Top->Top}. r.x r.x)
{x=lambda z:Top.z, y=lambda z:Top.z};
"hello";
unit;
lambda x:A. x;
let x=true in x;
{x=true, y=false};
{x=true, y=false}.x;
{true, false};
{true, false}.1;
if true then {x=true,y=false,a=false} else {y=false,x={},b=false};
timesfloat 2.0 3.14159;
lambda x:Bool. x;
(lambda x:Bool->Bool. if x false then true else false)
(lambda x:Bool. if x then false else true);
lambda x:Nat. succ x;
(lambda x:Nat. succ (succ x)) (succ 0);
T = Nat->Nat;
lambda f:T. lambda x:Nat. f (f x);