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