Stream: Coq users

Topic: Ampersand Syntax


view this post on Zulip Warrick Macmillan (Sep 21 2021 at 04:13):

what does the ampersand in Definitions mean, as in https://pastebin.com/Tg425qmD. Specifically, how would one translate the following to Agda : "Definition Foo := { Bar : foo1 & prod foo2 foo3 }"

view this post on Zulip Andrey Klaus (Sep 21 2021 at 07:23):

this does not work to me Definition VeridicalAdv := {Bar : nat & Foo : nat}.

view this post on Zulip Andrey Klaus (Sep 21 2021 at 07:25):

I think this is most likely kind of notation defined somewhere in library you use.

view this post on Zulip Andrey Klaus (Sep 21 2021 at 07:26):

I think you could try to provide working example, then somebody may give a better answer.

view this post on Zulip Théo Winterhalter (Sep 21 2021 at 08:23):

Yes it is defined, it just doesn't take colon on the right. It's the syntax for dependent sums. You can try Locate "&" and it will print a list of notations with & that you have in scope. Including

Notation "{ x : A & P }" := (sigT (fun x => P)) : type_scope
  (default interpretation)

view this post on Zulip Théo Winterhalter (Sep 21 2021 at 08:24):

Now you can type About sigT or Print sigT to learn more about it.

view this post on Zulip Ali Caglayan (Sep 21 2021 at 15:50):

To translate to agda, you will have to work with agdas sigma types

view this post on Zulip Warrick Macmillan (Sep 21 2021 at 18:06):

thank you. another question : is there any relation between Prop in Agda (approximately proof irrelevant types) and Prop in Coq ?

view this post on Zulip Gaëtan Gilbert (Sep 21 2021 at 18:35):

agda prop is more like coq sprop


Last updated: Feb 01 2023 at 12:30 UTC