diff options
| author | Marvin Borner | 2022-07-17 16:52:29 +0200 |
|---|---|---|
| committer | Marvin Borner | 2022-07-17 16:52:29 +0200 |
| commit | 313e883f5e2146a2005ae0ed6a36af835cbbc961 (patch) | |
| tree | 6e3e7f5c2445305d32b41a54180c500d456b18a5 /benchmark.bruijn | |
| parent | 15c5e04c598a19153404a1ac184ed36dd4b30160 (diff) | |
Features
very descriptive
Diffstat (limited to 'benchmark.bruijn')
| -rw-r--r-- | benchmark.bruijn | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/benchmark.bruijn b/benchmark.bruijn new file mode 100644 index 0000000..e11668f --- /dev/null +++ b/benchmark.bruijn @@ -0,0 +1,31 @@ +# ================== +# Lennart +# From Lambda-n-ways +# ================== + +true [[0]] +false [[1]] +if [[[2 0 1]]] +zero [[1]] +succ [[[0 2]]] +one succ zero +two succ one +three succ two +const [[1]] +pair [[[0 2 1]]] +fst [[1 0 [[1]]]] +snd [[1 0 [[0]]]] +fix [[1 (0 0)] [1 (0 0)]] +add fix [[[1 0 [succ (3 0 1)]]]] +mul fix [[[1 zero [add 1 (3 0 1)]]]] +fac fix [[0 one [mul 1 (2 0)]]] +eqnat fix [[[1 (0 true (const false)) [1 false [4 1 0]]]]] +sumto fix [[0 zero [add 1 (2 0)]]] +n5 add two three +n6 add three three +n17 add n6 (add n6 n5) +n37 succ (mul n6 n6) +n703 sumto n37 +n720 fac n6 + +main eqnat n720 (add n703 n17) = true |