Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-08-15 18:20:26 +03:00
Code Issues Projects Releases Wiki Activity

Add Lean benchmark

Browse Source
This commit is contained in:
Victor Maia 2022-07-14 20:22:44 -03:00
parent 40a8d38900
commit d41c85b4c1
2 changed files with 32 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
bench/README.md
View File

@ -16,6 +16,12 @@ time agda -i src file.agda
time idris2 --check file.idr
```
### Lean
```
time lean file.lean
```
### Kind2
```
@ -45,4 +51,5 @@ Kind2-C | 0.17 s
Kind2 | 0.58 s
Agda | 15.55 s
Idris2 | 67.40 s
Lean | timeout
```

25
bench/nat_exp.lean Normal file
View File

@ -0,0 +1,25 @@
inductive NAT where
| Z : NAT
| S : NAT -> NAT
inductive The : NAT -> Type where
| val : (x : NAT) -> The x
def add : NAT -> NAT -> NAT
| a, NAT.S b => NAT.S (add a b)
| a, NAT.Z => a
def mul : NAT -> NAT -> NAT
| a, NAT.S b => add a (mul a b)
| _, NAT.Z => NAT.Z
def exp : NAT -> NAT -> NAT
| a, NAT.S b => mul a (exp a b)
| _, NAT.Z => NAT.S NAT.Z
def nul : NAT -> NAT
| NAT.S a => nul a
| NAT.Z => NAT.Z
def work : The (nul (exp (NAT.S (NAT.S (NAT.S NAT.Z))) (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S NAT.Z))))))))))
:= @The.val NAT.Z