Stream: Elpi users & devs

Topic: Import Coq module in elpi file

view this post on Zulip Li-yao (Apr 05 2024 at 10:56):

Can I import a Coq module in an elpi file to use the imported notations in quotes?

view this post on Zulip Enrico Tassi (Apr 05 2024 at 13:40):

The elpi files are Accumulate (hence parsed/compiled) in a Coq context.

Require Import MyNotations.
Elpi Command x.
Elpi Accumulate File "f". (* this file can use the current Coq notations *)

view this post on Zulip Enrico Tassi (Apr 05 2024 at 13:42):

I a notation is not available, or a contant not defined, you get a Coq error. Elpu uses the Coq parser behind the scenes for the quoted code.

Last updated: Oct 13 2024 at 01:02 UTC