the next generation of the in-browser educational proof assistant
slightly more involved example
+61
+61
index.html
+61
index.html
···
596
596
|- by (3) {}}
597
597
s. 0 1 |- elim (M-Surround 1 "$s") {}}
598
598
</hol-string-proof>
599
+
<hol-string id="index.html/string-arithmetic" deps="index.html/myconfig">
600
+
-------- nat-z
601
+
(Nat Z)
602
+
603
+
n. (Nat n)
604
+
-------- nat-s
605
+
(Nat (S n))
606
+
607
+
n1.
608
+
-------- nat-plus-z
609
+
(Eval (Plus n1 Z) n1)
610
+
611
+
n1. n2. res.
612
+
(Eval (Plus n1 n2) res)
613
+
--------- nat-plus-s
614
+
(Eval (Plus n1 (S n2)) (S res))
615
+
616
+
------- string-zero
617
+
(Parse "0" Z)
618
+
619
+
------- string-one
620
+
(Parse "1" (S Z))
621
+
622
+
-------- string-two
623
+
(Parse "2" (S (S Z)))
624
+
625
+
-------- string-three
626
+
(Parse "3" (S (S (S Z))))
627
+
628
+
s1. s2. n2.
629
+
(Parse s2 n2)
630
+
--------- string-prod
631
+
(Parse "$s1 * $s2" (Prod s1 n2))
632
+
633
+
s1.
634
+
---------- eval-prod-Z
635
+
(Eval (Prod s1 Z) "")
636
+
637
+
s1. s1n. n.
638
+
(Eval (Prod s1 n) s1n)
639
+
----------- eval-prod-S
640
+
(Eval (Prod s1 (S n)) "$s1$s1n")
641
+
642
+
s. ast. res.
643
+
(Parse s ast)
644
+
(Eval ast res)
645
+
--------------- program-eval
646
+
(PEval s res)
647
+
648
+
</hol-string>
649
+
<hol-string-proof id="index.html/sexp-nat-toy" deps="index.html/myconfig index.html/string-arithmetic">
650
+
----------- mexp-lexp
651
+
(Eval (Plus (S Z) (S (S Z))) (S (S (S Z))))
652
+
|- ?
653
+
</hol-string-proof>
654
+
<hol-string-proof id="index.html/string-prod-toy" deps="index.html/myconfig index.html/string-arithmetic">
655
+
------------- foo-3
656
+
(PEval "foo * 3" "foo foo foo")
657
+
|- ?
658
+
659
+
</hol-string-proof>
599
660
<script type="module" src="./src/testcomponent.tsx"></script>
600
661
</body>
601
662
</html>