Skip to content

Commit b8578d9

Browse files
authored
Revise ELPI.md for declare_constraint and mode updates
Updated ELPI documentation to clarify the usage of declare_constraint and changed mode declarations to func.
1 parent e905c06 commit b8578d9

File tree

1 file changed

+7
-7
lines changed

1 file changed

+7
-7
lines changed

ELPI.md

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -664,10 +664,10 @@ goal> pi x\ sigma Y\ even x => (declare_constraint (even Y) [Y], Y = x).
664664
Success:
665665
```
666666

667-
The `declare_constraint` built in is typically used in conjunction with `mode`
668-
as follows:
667+
The `declare_constraint` built requires functions, and is typically
668+
used as follows:
669669
```prolog
670-
mode (even i).
670+
func even int -> .
671671
even (uvar as X) :- !, declare_constraint (even X) [X].
672672
even 0.
673673
even X :- X > 1, Y is X - 2, even Y.
@@ -753,8 +753,8 @@ It is used only in debug output.
753753

754754
#### Example
755755
```prolog
756-
mode (odd i).
757-
mode (even i).
756+
func odd int -> .
757+
func even int -> .
758758
759759
even (uvar as X) :- !, declare_constraint (even X) [X].
760760
odd (uvar as X) :- !, declare_constraint (odd X) [X].
@@ -803,7 +803,7 @@ we can compute GCDs of 2 sets of numbers: 99, 66 and 22 named X;
803803
14 and 77 called Y.
804804

805805
```prolog
806-
mode (gcd i i).
806+
func gcd int ,int -> .
807807
808808
gcd A (uvar as Group) :- declare_constraint (gcd A Group) Group.
809809
@@ -827,7 +827,7 @@ Constraints are resumed as regular delayed goals are.
827827
#### Example of higher order rules
828828

829829
```prolog
830-
mode (term i o).
830+
func term tm -> ty.
831831
term (app HD ARG) TGT :- term HD (arrow SRC TGT), term ARG SRC.
832832
term (lam F) (arrow SRC TGT) :- pi x\ term x SRC => term (F x) TGT.
833833
term (uvar as X) T :- declare_constraint (term X T) [X].

0 commit comments

Comments
 (0)