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