[Agda] A question on why "postulate" works but "variable" fails

[Eduardo Ochs]

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>