Stream: Coq users

Topic: Use external vars inside custom entry


view this post on Zulip 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?

view this post on Zulip Notification Bot (Jan 11 2022 at 11:19):

Julin S has marked this topic as resolved.

view this post on Zulip Notification Bot (Jan 11 2022 at 11:19):

Julin S has marked this topic as unresolved.

view this post on Zulip Notification Bot (Jan 11 2022 at 11:19):

Julin S has marked this topic as resolved.

view this post on Zulip Notification Bot (Jan 11 2022 at 11:20):

Julin S has marked this topic as unresolved.

view this post on Zulip Julin S (Jan 11 2022 at 11:20):

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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jan 11 2022 at 18:40):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 12 2022 at 04:39):

(deleted)

view this post on Zulip 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: Jan 28 2023 at 06:30 UTC