feat(emacs): Path induction snippet
This commit is contained in:
@@ -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 = ?
|
||||||
Reference in New Issue
Block a user