diff --git a/bench/README.md b/bench/README.md
index 5614657a..3855ec44 100644
--- a/bench/README.md
+++ b/bench/README.md
@@ -4,19 +4,25 @@ Bench
 Benchmarks of Kind2 vs other proof assistants. These benchmarks measure the time
 each assistant takes to verify a given file. Replicate as follows:
 
-### Agda:
+### Agda
 
 ```
 time agda -i src file.agda
 ```
 
-### Kind2-i (interpreted HVM)
+### Idris2
+
+```
+time idris2 --check file.idr
+```
+
+### Kind2
 
 ```
 time kind2 check file.kind2
 ```
 
-### Kind2-c (compiled HVM)
+### Kind2-C
 
 ```
 kind2 check file.kind2
@@ -28,14 +34,15 @@ time ./check
 Results
 =======
 
-### slow_num
+### nat_exp
 
-Computes `2 ^ 24`, using the Nat type, on the type level. 
+Computes `3 ^ 8`, using the Nat type, on the type level.
 
 ```
 language | time
 -------- | --------
-Agda     | 11.277 s
-Kind2-i  |  2.350 s 
-Kind2-c  |  0.925 s
+Kind2-C  |   0.17 s
+Kind2    |   0.58 s
+Agda     |  15.55 s
+Idris2   |  67.40 s
 ```
diff --git a/bench/nat_exp.agda b/bench/nat_exp.agda
new file mode 100644
index 00000000..799345ea
--- /dev/null
+++ b/bench/nat_exp.agda
@@ -0,0 +1,25 @@
+data Nat : Set where
+  z : Nat
+  s : Nat -> Nat
+
+data The : (x : Nat) -> Set where
+  val : (x : Nat) -> The x
+
+add : Nat -> Nat -> Nat
+add a (s b) = s (add a b)
+add a z     = a
+
+mul : Nat -> Nat -> Nat
+mul a (s b) = add a (mul a b)
+mul a z     = z
+
+exp : Nat -> Nat -> Nat
+exp a (s b) = mul a (exp a b)
+exp a     z = s z
+
+nul : Nat -> Nat
+nul (s a) = (nul a)
+nul z     = z
+
+work : The (nul (exp (s (s (s z))) (s (s (s (s (s (s (s (s z))))))))))
+work = val z
diff --git a/bench/nat_exp.idr b/bench/nat_exp.idr
new file mode 100644
index 00000000..13c3a196
--- /dev/null
+++ b/bench/nat_exp.idr
@@ -0,0 +1,26 @@
+data NAT : Type where
+  Z : NAT
+  S : NAT -> NAT
+
+data The : NAT -> Type where
+  Val : (x : NAT) -> The x
+
+add : NAT -> NAT -> NAT
+add a (S b) = S (add a b)
+add a Z     = a
+
+mul : NAT -> NAT -> NAT
+mul a (S b) = add a (mul a b)
+mul a Z     = Z
+
+exp : NAT -> NAT -> NAT
+exp a (S b) = mul a (exp a b)
+exp a     Z = S Z
+
+nul : NAT -> NAT
+nul (S a) = nul a
+nul Z     = Z
+
+work : The (nul (exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))
+work = Val Z
+
diff --git a/bench/nat_exp.kind2 b/bench/nat_exp.kind2
new file mode 100644
index 00000000..b3d05b3e
--- /dev/null
+++ b/bench/nat_exp.kind2
@@ -0,0 +1,29 @@
+Nat : Type
+  Z             : Nat
+  S (pred: Nat) : Nat
+
+The (x: Nat) : Type
+  Val (x: Nat) : {The x}
+
+Add (a: Nat) (b: Nat) : Nat {
+  Add a {S b} = {S (Add a b)}
+  Add a {Z}   = a
+}
+
+Mul (a: Nat) (b: Nat) : Nat {
+  Mul a {S b} = (Add a (Mul a b))
+  Mul a {Z}   = {Z}
+}
+
+Exp (a: Nat) (b: Nat) : Nat {
+  Exp a {S b} = (Mul a (Exp a b))
+  Exp a {Z}   = {S Z}
+}
+
+Nul (n: Nat) : Nat {
+  Nul {S a}     = (Nul a)
+  Nul {Z}       = {Z}
+}
+
+Work : {The (Nul (Exp {S {S {S Z}}} {S {S {S {S {S {S {S {S Z}}}}}}}}))} =
+  {Val Z}
diff --git a/bench/slow_num.agda b/bench/slow_num.agda
deleted file mode 100644
index 7a1c1ca1..00000000
--- a/bench/slow_num.agda
+++ /dev/null
@@ -1,39 +0,0 @@
-data Nat : Set where
-  zero : Nat
-  succ : Nat -> Nat
-
-data The : (x : Nat) -> Set where
-  val : (x : Nat) -> The x
-
-double : (x : Nat) -> Nat
-double (succ x) = (succ (succ (double x)))
-double zero     = zero
-
-power2 : (x : Nat) -> Nat
-power2 (succ x) = (double (power2 x))
-power2 zero     = (succ zero)
-
-destroy : (x : Nat) -> Nat
-destroy (succ n) = (destroy n)
-destroy zero     = zero
-
-slowNumber : Nat
-slowNumber =
-  (destroy (power2
-    (succ (succ (succ (succ
-    (succ (succ (succ (succ
-    (succ (succ (succ (succ
-    (succ (succ (succ (succ
-    (succ (succ (succ (succ
-    (succ (succ (succ (succ
-    zero
-    ))))
-    ))))
-    ))))
-    ))))
-    ))))
-    ))))
-  ))
-
-main : The slowNumber
-main = val zero
diff --git a/bench/slow_num.kind2 b/bench/slow_num.kind2
deleted file mode 100644
index bd413939..00000000
--- a/bench/slow_num.kind2
+++ /dev/null
@@ -1,41 +0,0 @@
-Nat : Type
-  Zero             : Nat
-  Succ (pred: Nat) : Nat
-
-The (x: Nat) : Type
-  Val (x: Nat) : {The x}
-
-Double (x: Nat) : Nat {
-  Double {Succ x} = {Succ {Succ (Double x)}}
-  Double {Zero}   = {Zero}
-}
-
-Pow2 (x: Nat) : Nat {
-  Pow2 {Succ x} = (Double (Pow2 x))
-  Pow2 {Zero}   = {Succ Zero}
-}
-
-Destroy (x: Nat) : Nat {
-  Destroy {Succ n} = (Destroy n)
-  Destroy {Zero}   = {Zero}
-}
-
-SlowNumber : Nat =
-  (Destroy (Pow2
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    {Succ {Succ {Succ {Succ
-    Zero
-    }}}}
-    }}}}
-    }}}}
-    }}}}
-    }}}}
-    }}}}
-  ))
-  
-// Proof that SlowNumber is 0
-Main : {The (SlowNumber)} = {Val Zero}