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 }"
this does not work to me Definition VeridicalAdv := {Bar : nat & Foo : nat}.
I think this is most likely kind of notation defined somewhere in library you use.
I think you could try to provide working example, then somebody may give a better answer.
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)
Now you can type About sigT
or Print sigT
to learn more about it.
To translate to agda, you will have to work with agdas sigma types
thank you. another question : is there any relation between Prop in Agda (approximately proof irrelevant types) and Prop in Coq ?
agda prop is more like coq sprop
Last updated: Oct 13 2024 at 01:02 UTC