-- This file: -- http://angg.twu.net/AGDA/Postulate1.agda.html -- http://angg.twu.net/AGDA/Postulate1.agda -- (find-angg "AGDA/Postulate1.agda") -- Author: Eduardo Ochs -- Version: 2021dec28 (with tiny changes later) -- Public domain. -- -- Long story short: if we want to build telescopes for tests the -- right tool to use is "postulate", not "variable". See: -- https://lists.chalmers.se/pipermail/agda/2021/012832.html my question -- https://lists.chalmers.se/pipermail/agda/2021/012834.html Jesper's answer =) -- My failed attempt to use "variable"s is here: -- (find-angg "AGDA/Variable1.agda") -- -- This file takes some examples of the old RecordsTutorial and makes -- them more concrete by specializing the "n" and the "m" in the -- length of its telescopes to 2 and 2. -- -- The sexp hyperlinks with `page' and `text' are explained here: -- (find-pdf-like-intro "7. Shorter hyperlinks to PDF files") -- -- ;; (find-eev "eev-pdflike.el" "change-default-viewer") -- ;; (defalias 'find-pdf-page 'find-pdftools-page) -- ;; (defalias 'find-pdf-page 'find-xpdf-page) -- -- https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening -- (find-recordstutorialpage 13 "Opening a record") -- (find-recordstutorialtext 13 "Opening a record") -- -- ;; (find-angg "AGDA/find-agdatype.el" "video-0") -- ;; (find-angg "AGDA/find-agdatype.el") -- (load "~/AGDA/find-agdatype.el") module Postulate1 where -- From: -- https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#syntax -- (find-recordstutorialpage 12 "General Syntax and Meaning") -- (find-recordstutorialtext 12 "General Syntax and Meaning") -- -- General Syntax and Meaning -- A record type in general is declared in the following way. -- -- record R Δ : Set where -- field -- x₁ : A₁[y₁, ..., yₘ₋₁] -- x₂ : A₁[y₁, ..., yₘ₋₁, x₁] -- ... -- xₙ : A₁[y₁, ..., yₘ₋₁, x₁, ..., xₙ₋₁] -- -- Here, Δ represents a 'telescope', which is of the following form -- -- (y₁ : B₁) (y₂ : B₂[y₁]) ... (yₘ : Bₘ[y₁, ..., yₘ₋₁]) -- -- Let's make m:=2 and n:=2. -- Then... 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 -- (find-agdatype " B₁ ") -- (find-agdatype " B₂ ") -- (find-agdatype " A₁ ") -- (find-agdatype " A₂ ") -- postulate y₁ : B₁ -- postulate y₂ : B₂ y₁ -- postulate x₁ : A₁ y₁ y₂ -- postulate x₂ : A₂ y₁ y₂ x₁ ---- ^ These postulates were useful in my first tests, but their names ---- started to collide with other things and I had to comment them ---- out... ---- (find-agdatype " y₁ ") ---- (find-agdatype " y₂ ") ---- (find-agdatype " x₁ ") ---- (find-agdatype " x₂ ") ---- (find-agdatype " B₁ ") ---- (find-agdatype " B₂ y₁ ") ---- (find-agdatype " A₁ y₁ y₂ ") ---- (find-agdatype " A₂ y₁ y₂ x₁ ") record R (y₁ : B₁) (y₂ : B₂ y₁) : Set1 where field x₁ : A₁ y₁ y₂ x₂ : A₂ y₁ y₂ x₁ postulate ay₁ : B₁ postulate ay₂ : B₂ ay₁ postulate ax₁ : A₁ ay₁ ay₂ postulate ax₂ : A₂ ay₁ ay₂ ax₁ postulate ar : R ay₁ ay₂ -- (find-recordstutorialpage 13 "This declaration introduces") -- (find-recordstutorialtext 13 "This declaration introduces") -- (find-agdatype " R ") -- (find-agdatype " R.x₁ ") -- (find-agdatype " R.x₂ ") -- (find-agdatype " ar ") -- (find-agdatype " R.x₁ ar ") -- (find-agdatype " R.x₂ ar ") -- (find-agdatype " R ay₁ ") -- (find-agdatype " R ay₁ ay₂ ") -- From: -- https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening -- (find-recordstutorialpage 13 "Opening a record") -- (find-recordstutorialtext 13 "Opening a record") -- (...) For the record R above, we generate a parametrised module R: -- -- module R {Δ} (r : R Δ) where -- x₁ : A₁[y₁, ..., yₘ₋₁] -- x₁ = ... -- x₂ : A₂[y₁, ..., yₘ₋₁, x₁] -- x₂ = ... -- ... -- xₙ : Aₙ[y₁, ..., yₘ₋₁, x₁, ..., xₙ₋₁] -- xₙ = ... module MR {y₁ : B₁} {y₂ : B₂ y₁} (r : R y₁ y₂) where x₁ : A₁ y₁ y₂ x₁ = {!!} x₂ : A₂ y₁ y₂ x₁ x₂ = {!!} -- (find-recordstutorialpage 14 "Record opening example") -- (find-recordstutorialtext 14 "Record opening example") -- (find-agdatype " MR.x₁ ") -- (find-agdatype " MR.x₂ ") -- (find-agdatype " MR.x₁ ar ") -- (find-agdatype " MR.x₂ ar ") module TestOpen where open MR ar goal : {!!} goal = {!!} -- (find-agdatype " x₁ ") -- (find-agdatypep " x₁ ") -- ^ Note that here `find-agdatype' doesn't work, -- but `find-agdatypep' does... -- Local Variables: -- coding: utf-8-unix -- End: