[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,

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₁

and this in the file /tmp/test/V.agda:

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₁

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

I just spent some hours trying to understand the section 3.14 -
"Generalization of Declared Variables", link:


- 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

P.S.: I am using Agda

P.P.S.: To be honest I was trying to understand this,
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