the next generation of the in-browser educational proof assistant
add example showing type coercion failure
+21
+21
index.html
+21
index.html
···
657
657
|- ?
658
658
659
659
</hol-string-proof>
660
+
<hol-string id="index.html/string-silliness" deps="index.html/myconfig">
661
+
a.
662
+
-------------- eq-refl
663
+
(Eq a a)
664
+
665
+
a. b. (Eq a b)
666
+
-------------- eq-sym
667
+
(Eq b a)
668
+
669
+
a. b. c. (Eq a b) (Eq "$b" c)
670
+
-------------- eq-trans-weird
671
+
(Eq a c)
672
+
673
+
-------------- eq-a-comp
674
+
(Eq "a" (Foo Bar))
675
+
</hol-string>
676
+
<hol-string-proof id="index.html/string-silliness-trip" deps="index.html/myconfig index.html/string-silliness">
677
+
------------- eq-a-c
678
+
(Eq "a" "a")
679
+
|- ?
680
+
</hol-string-proof>
660
681
<script type="module" src="./src/testcomponent.tsx"></script>
661
682
</body>
662
683
</html>