feat(emacs): agda __cubical file template
This commit is contained in:
19
modules/home/users/crumb/emacs/snippets/agda2-mode/__cubical
Normal file
19
modules/home/users/crumb/emacs/snippets/agda2-mode/__cubical
Normal file
@@ -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
|
||||||
Reference in New Issue
Block a user