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