Stream: Coq users

Topic: Use external vars inside custom entry

Julin S (Jan 11 2022 at 11:19):

Is there a way to use variables defined outside the scope of a custom entry inside the scope of the same custom entry?

I did something like

Declare Custom Entry cename.

Notation "{{ e }}" := (e) (e custom cename at level 100).

Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..)
  (in custom cename at level 50, x constr).

Require Import List.
Import ListNotations.

Notation "x ++ y" := (x ++ y)
  (in custom cename at level 50).
  (* not sure why but having [x constr] here led to error *)


Compute {{ [1;2] }}.
Compute {{ [1;2] ++ [3;4] }}.

and was trying to do

Definition foo := [1;2]%list.

Compute {{ [1;2] ++ foo }}.

ie, to use foo inside the {{ .. }}.

Is this possible?

Notification Bot (Jan 11 2022 at 11:19):

Julin S has marked this topic as resolved.

Notification Bot (Jan 11 2022 at 11:19):

Julin S has marked this topic as unresolved.

Notification Bot (Jan 11 2022 at 11:19):

Julin S has marked this topic as resolved.

Notification Bot (Jan 11 2022 at 11:20):

Julin S has marked this topic as unresolved.

Julin S (Jan 11 2022 at 11:20):

Been trying to edit topic title but I keep clicking on checkmark instead... :sweat_smile:

Paolo Giarrusso (Jan 11 2022 at 18:39):

not sure but is this answered in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.E2.9C.94.20Making.20a.20custom.20entry?

Paolo Giarrusso (Jan 11 2022 at 18:40):

"using foo" is a constr so x, y constr should help

Julin S (Jan 12 2022 at 04:22):

No, although I had a similar issue as part of this, that was something else. The doubt in this post was about using definition defined outside the custom entry 'scope' inside the custom entry notations.

Paolo Giarrusso (Jan 12 2022 at 04:39):

(deleted)

Julin S (Jan 12 2022 at 06:22):

I wasn't sure if the solution for this calls for something more complex. I was sort of taking inspiration from koika. They seem to doing something non-simple (using something named UBind and a notation let ... in) but haven't yet grasped how to mimick that.

Last updated: Apr 18 2024 at 22:02 UTC