fmt

Author: 5HT

index.html

@@ -27,8 +27,8 @@
 Main commands are check (to check a program) and repl (to enter the proof shell).
 </p><code>$ opam install anders</code><p>Anders is fast, idiomatic and educational. We carefully draw the favourite
 Lean-compatible syntax to fit 200 LOC in Menhir.
-The CHM kernel is 1K LOC. Whole Anders compiles under 2 seconds
-and checks all the base library under 1 second [i7-8700].
+The CHM kernel is 1K LOC. Whole Anders compiles under 1 second
+and checks all the base library under 1/3 of a second [i5-12400].
 <b>Anders</b> proof assistant as Homotopy Type System comes
 with its own <a href="https://anders.groupoid.space/lib/">Homotopy Library</a>.
 </p><code>$ anders help

index.pug

@@ -78,8 +78,8 @@ block content
                 p.
                     Anders is fast, idiomatic and educational. We carefully draw the favourite
                     Lean-compatible syntax to fit 200 LOC in Menhir.
-                    The CHM kernel is 1K LOC. Whole Anders compiles under 2 seconds
-                    and checks all the base library under 1 second [i7-8700].
+                    The CHM kernel is 1K LOC. Whole Anders compiles under 1 second
+                    and checks all the base library under 1/3 of a second [i5-12400].
                     <b>Anders</b> proof assistant as Homotopy Type System comes
                     with its own <a href="https://anders.groupoid.space/lib/">Homotopy Library</a>.