Stream: Elpi users & devs

Topic: When does coq.elpi.accumulate take effect?


view this post on Zulip Michael Soegtrop (Nov 10 2022 at 14:47):

Building on the age example from the tutorial I wrote this code:

Require Import elpi.elpi.

Elpi Db age.db lp:{{
  pred age o:string, o:int.
  :name "age.fail"
  age Name _ :- coq.error "I don't know who" Name "is!".
}}.

Elpi Command set_age.
Elpi Accumulate Db age.db.
Elpi Accumulate lp:{{
  main [str Name, int Age] :-
    coq.say "Pre" Name Age,
    coq.elpi.accumulate _ "age.db" (clause _ (before "age.fail") (age Name Age)),
    age Name AgeDb,
    coq.say "Post" Name AgeDb.
}}.
Elpi Typecheck.

Elpi set_age "alice" 21.

The age query in the set_age main function fails, so obviously the statement has not yet been added at this point. I wonder what the rules are here.


Last updated: Feb 04 2023 at 02:03 UTC