You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi. It looks like it is not possible to add a clause to a predicate immediately after the creation of the predicate, as the following code shows.
From elpi.apps Require Import tc.
Record C : Prop := {}.
Elpi Query TC.Solver lp:{{
global R = {{ C }},
coq.TC.declare-class R,
coq.elpi.accumulate current "tc.db" (clause _ _ {coq.elpi.predicate {gref->pred-name R} [Build_C]}).
}}.
This fails with the error message
Anomaly
"Uncaught exception Elpi__Compiler.CompileError(0, "allocating new global symbol 'tc-buffer4.tc-C' at runtime")."
The text was updated successfully, but these errors were encountered:
Hi. It looks like it is not possible to add a clause to a predicate immediately after the creation of the predicate, as the following code shows.
This fails with the error message
The text was updated successfully, but these errors were encountered: