[Agda] A question about the innards of C-c C-d
Eduardo Ochs
eduardoochs at gmail.com
Tue Dec 28 00:21:51 CET 2021
Hi list,
if we define the function eek in Elisp as:
(defun eek (str)
"Execute STR as a keyboard macro. See `edmacro-mode' for the exact
format.\n
An example: (eek \"C-x 4 C-h\")"
(interactive "sKeys: ")
(execute-kbd-macro (read-kbd-macro str)))
and we create a file /tmp/test/T.agda containing this,
--snip--snip--
open import Level
MySet1 : Set₂
MySet1 = Set (Level.suc Level.zero)
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
record R (y₁ : B₁) (y₂ : B₂ y₁) : MySet1 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₂
-- (eek "C-a C-c C-d R RET")
-- (eek "C-a C-c C-d R.x₁ RET")
-- (eek "C-a C-c C-d R.x₂ RET")
-- (eek "C-a C-c C-d ar RET")
-- (eek "C-a C-c C-d R.x₁ SPC ar RET")
--snip--snip--
then the sexps with "eek" work as buttons that can be executed with
C-e C-x C-e, and whose effects are to display the types of the
expressions "R", "R.x₁", "R.x₂", "ar", and "R.x₁ ar" in the second
window... note that the "R.x₁ SPC ar" in the last sexp was sort of
translated to "R.x₁ ar".
I am looking for a better way to do that, but I am having trouble to
understand the innards of the function bound to C-c C-d -
agda2-infer-type-maybe-toplevel - because it uses at least two levels
of macros...
So: suppose that I define foo as:
(defun foo ()
"Running M-x foo in agda2-mode should be equivalent to
typing C-c C-d R.x₁ ar RET"
(interactive)
(bar "R.x₁ ar"))
what is the right way to define bar in a low-level way? Let's suppose
for simplicity that we just want to make this work in situations in
which agda2-infer-type-maybe-toplevel would run
agda2-infer-type-toplevel, and we don't care for the cases in which it
would run agda2-infer-type...
Thanks in advance!
Eduardo Ochs
http://angg.twu.net/#eev
http://angg.twu.net/eev-intros/find-eev-quick-intro.html#3
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211227/b256d9e5/attachment-0001.html>
More information about the Agda
mailing list