From e1363f60ab33d6c49d084e2621c2d0a919b5f324 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Madeleine=20Sydney=20=C5=9Alaga?= Date: Tue, 11 Nov 2025 00:40:32 -0700 Subject: [PATCH] feat(emacs): agda __cubical file template --- .../crumb/emacs/snippets/agda2-mode/__cubical | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 modules/home/users/crumb/emacs/snippets/agda2-mode/__cubical diff --git a/modules/home/users/crumb/emacs/snippets/agda2-mode/__cubical b/modules/home/users/crumb/emacs/snippets/agda2-mode/__cubical new file mode 100644 index 0000000..e9c2176 --- /dev/null +++ b/modules/home/users/crumb/emacs/snippets/agda2-mode/__cubical @@ -0,0 +1,19 @@ +# -*- mode: snippet -*- +# name: __cubical +# key: __cubical +# -- +{-# OPTIONS --safe --guardedness --cubical --without-K #-} + +module ${1:Module} where + +open import Cubical.Foundations.Prelude +-- open import Cubical.Data.Sigma +-- open import Cubical.HITs.PropositionalTruncation +-- open import Cubical.Foundations.Function +-- open import Cubical.Foundations.Function + + +private variable + ℓ ℓ' ℓ'' : Level + +$2 \ No newline at end of file