liamoc.net / holbert-ng
the next generation of the in-browser educational proof assistant
1
fork

Configure Feed

Select the types of activity you want to include in your feed.

example

Josh Brown 6acdd385 9f32fdb4

+10
+10
index.html
··· 546 546 ------------------- MParse-Juxtapose 547 547 "$s1 $s2" (MP (p1 p2)) 548 548 </hol-string> 549 + <hol-string id="index.html/string-rhs" deps="index.html/myconfig"> 550 + ---- Expr-e 551 + "e" (Expr e) 552 + 553 + s1. 554 + s2. e2. 555 + "$s2" (Expr e2) 556 + ------------- Stmt-Let 557 + "let $s1 = $s2" (Let (ID s1) e2) 558 + </hol-string> 549 559 <hol-string id="index.html/mexp-induct" deps="index.html/myconfig"> 550 560 s. p. 551 561 "$s" M "" p [s1. "$s1" p |- "($s1)" p] [s1. s2. "$s1" p "$s2" p |- "$s1 $s2" p]