Skip to content

Commit 0f644ad

Browse files
committed
doc
1 parent 919c130 commit 0f644ad

File tree

1 file changed

+13
-3
lines changed

1 file changed

+13
-3
lines changed

ELPI.md

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -241,10 +241,10 @@ such clause using the `:before` attribute.
241241
fatal-error Msg :- !, M is "elpi: " ^ Msg, coq-err M.
242242
```
243243

244-
The `:after` and `:replace` attributes is also available.
244+
The `:after`, `:replace` and `:remove` attributes is also available.
245245

246-
The `:replace` attribute cannot be given to a named clause. This is to avoid
247-
the following ambiguity:
246+
The `:replace` and `:remove` attribute cannot be given to a named clause.
247+
This is to avoid the following ambiguity:
248248

249249
```prolog
250250
:name "replace-me"
@@ -260,6 +260,16 @@ p 3.
260260
```
261261
Here the order in which replacement is performed would matter.
262262

263+
Both `:replace:` and `:remove` can only apply to rules for the same predicate.
264+
Example:
265+
266+
```prolog
267+
:name "this" p 1.
268+
269+
:remove "this" p _. % OK
270+
:remove "this" q _. % Error
271+
```
272+
263273

264274
## Conditional compilation
265275

0 commit comments

Comments
 (0)