init
This commit is contained in:
7
snippets/coq-mode/definitions/definition.yasnippet
Normal file
7
snippets/coq-mode/definitions/definition.yasnippet
Normal file
@@ -0,0 +1,7 @@
|
||||
# -*- mode: snippet -*-
|
||||
# key: Def
|
||||
# group: definitions
|
||||
# name: Definition
|
||||
# --
|
||||
Definition $1 ($2 : $3) : $4 :=
|
||||
$0.
|
||||
9
snippets/coq-mode/definitions/fixpoint-with.yasnippet
Normal file
9
snippets/coq-mode/definitions/fixpoint-with.yasnippet
Normal file
@@ -0,0 +1,9 @@
|
||||
# -*- mode: snippet -*-
|
||||
# key: Fixpw
|
||||
# group: definitions
|
||||
# name: Fixpoint-with
|
||||
# --
|
||||
Fixpoint $1 ($2 : $3) : $4 :=
|
||||
$9
|
||||
with $5 ($6 : $7) : $8 :=
|
||||
$0.
|
||||
7
snippets/coq-mode/definitions/fixpoint.yasnippet
Normal file
7
snippets/coq-mode/definitions/fixpoint.yasnippet
Normal file
@@ -0,0 +1,7 @@
|
||||
# -*- mode: snippet -*-
|
||||
# key: Fixp
|
||||
# group: definitions
|
||||
# name: Fixpoint
|
||||
# --
|
||||
Fixpoint $1 ($2 : $3) : $4 :=
|
||||
$0.
|
||||
6
snippets/coq-mode/definitions/fun.yasnippet
Normal file
6
snippets/coq-mode/definitions/fun.yasnippet
Normal file
@@ -0,0 +1,6 @@
|
||||
# -*- mode: snippet -*-
|
||||
# key: fun
|
||||
# group: definitions
|
||||
# name: fun
|
||||
# --
|
||||
fun ($1 : $2 => $0)
|
||||
8
snippets/coq-mode/definitions/inductive.yasnippet
Normal file
8
snippets/coq-mode/definitions/inductive.yasnippet
Normal file
@@ -0,0 +1,8 @@
|
||||
# -*- mode: snippet -*-
|
||||
# key: Ind
|
||||
# group: definitions
|
||||
# name: Inductive
|
||||
# --
|
||||
Inductive $1 : $2 :=
|
||||
| $0
|
||||
.
|
||||
Reference in New Issue
Block a user