From 331233b1789d27fbe1557f3e03333257d5fbf39a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Madeleine=20Sydney=20=C5=9Alaga?= Date: Sun, 23 Nov 2025 07:30:27 -0700 Subject: [PATCH] feat(emacs): Path induction snippet --- .../msyds/emacs/snippets/agda2-mode/Path induction | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 modules/home/users/msyds/emacs/snippets/agda2-mode/Path induction diff --git a/modules/home/users/msyds/emacs/snippets/agda2-mode/Path induction b/modules/home/users/msyds/emacs/snippets/agda2-mode/Path induction new file mode 100644 index 0000000..0584b43 --- /dev/null +++ b/modules/home/users/msyds/emacs/snippets/agda2-mode/Path induction @@ -0,0 +1,10 @@ +# -*- mode: snippet -*- +# name: J D d where +# key: J +# expand-env: ((yas-indent-line 'fixed)) +# -- +J D d where + D : (y : ?) → ? ≡ ? → Type ? + D y p = ? + d : D ? refl + d = ? \ No newline at end of file