[Agda] A question on why "postulate" works but "variable" fails
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!
P.S.: I am using Agda 18.104.22.168.
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...
More information about the Agda