[Agda] A question on why "postulate" works but "variable" fails
Eduardo Ochs
eduardoochs at gmail.com
Mon Dec 27 23:20:09 CET 2021
Hi! Help! Beginner question!
Let me start with instructions to reproduce the problem.
Put this in the file /tmp/test/P.agda,
--snip--snip--
postulate B₁ : Set
postulate B₂ : (y₁ : B₁) → Set
postulate A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) → Set
postulate A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
postulate y₁ : B₁
postulate y₂ : B₂ y₁
postulate x₁ : A₁ y₁ y₂
postulate x₂ : A₂ y₁ y₂ x₁
--snip--snip--
and this in the file /tmp/test/V.agda:
--snip--snip--
variable B₁ : Set
variable B₂ : (y₁ : B₁) → Set
variable A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) → Set
variable A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
variable y₁ : B₁
variable y₂ : B₂ y₁
variable x₁ : A₁ y₁ y₂
variable x₂ : A₂ y₁ y₂ x₁
--snip--snip--
When I use the key sequence `C-c C-l' from agda2-mode to load the two
files in the file P.agda everything works, but in V.agda I get an
error whose main message is "Failed to solve the following
constraints"... and in another case in which I was working using
"postulate" worked, but when I used "variable" I got an error that
started with something like "Generalizable variables not allowed
here".
I just spent some hours trying to understand the section 3.14 -
"Generalization of Declared Variables", link:
https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=83
- of the user manual, but it's too terse for me and it has too many
prerequisites, and I am stuck.
So, QUESTION: can you recommend me other places to learn the
distinctions between "postulate" and "variable"?
Thanks in advance!
Eduardo Ochs
http://angg.twu.net/math-b.html
P.S.: I am using Agda 2.6.1.3.
P.P.S.: To be honest I was trying to understand this,
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening
and to specialize its example to n:=2 and m:=2 and to check if the
"(r : R Δ)" really works, but I have the impression that I need to
understand variables first...
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211227/53bc85a7/attachment.html>
More information about the Agda
mailing list