Skip to content

Commit

Permalink
add comment in tutorial (Deducteam#1132)
Browse files Browse the repository at this point in the history
  • Loading branch information
fblanqui authored Aug 30, 2024
1 parent 230d572 commit 82d2d39
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion tests/OK/tutorial.lp
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,12 @@
visualize this file and the generated subgoals in proofs
(this is a multi-lines comment). */

/* Put this file and
https://github.com/Deducteam/lambdapi/blob/master/tests/lambdapi.pkg
in the same directory, and run emacs or vscode from this
directory. Make sure that lambdapi is in your path (do "eval `opam
env`" if you installed lambdapi with opam). */

/* In Lambdapi, you can declare type and object symbols. Symbol names
can contain unicode characters (utf8). */

Expand Down Expand Up @@ -65,7 +71,7 @@ assert ⊢ zero + zero ≡ zero;
// The definition of + can be completed by adding a new rule later:
rule $x + succ $y ↪ succ ($x + $y);

// Several rules can also be given as once:
// Several rules can also be given at once:
rule zero × $y ↪ zero
with succ $x × $y ↪ $y + $x × $y;

Expand Down

0 comments on commit 82d2d39

Please sign in to comment.