Adds snippets for coq-mode

This commit is contained in:
Peter Urbak 2019-10-06 22:09:59 +02:00
parent 52e4be5acd
commit 2eac2f8b6f
39 changed files with 295 additions and 0 deletions

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: Def
# group: definitions
# name: Definition
# --
Definition $1 ($2 : $3) : $4 :=
$0.

View 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.

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: Fixp
# group: definitions
# name: Fixpoint
# --
Fixpoint $1 ($2 : $3) : $4 :=
$0.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: fun
# group: definitions
# name: fun
# --
fun ($1 : $2 => $0)

View file

@ -0,0 +1,8 @@
# -*- mode: snippet -*-
# key: Ind
# group: definitions
# name: Inductive
# --
Inductive $1 : $2 :=
| $0
.

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: C
# group: lookup
# name: Check
# --
Check $1.
$0

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: L
# group: lookup
# name: Locate
# --
Locate "$1".
$0

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: P
# group: lookup
# name: Print
# --
Print $1.
$0

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: S
# group: lookup
# name: Search
# --
Search $1.
$0

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: SA
# group: lookup
# name: SearchAbout
# --
SearchAbout $1.
$0

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: SP
# group: lookup
# name: SearchPattern
# --
SearchPattern ($1).
$0

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: fa
# group: misc
# name: forall
# --
forall ($1 : $2), $0

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: if
# group: misc
# name: if
# --
if $1 then $2 else $0

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: Inf
# group: misc
# name: Infix
# --
Infix "$1" := $2 (at level $3, $4 associativity).
$0

View file

@ -0,0 +1,8 @@
# -*- mode: snippet -*-
# key: match
# group: misc
# name: match
# --
match $1 with
| $0 =>
end

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: Nota
# group: misc
# name: Notation
# --
Notation "$1" := ($2) (at level $3, $4 associativity).
$0

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: Req
# group: misc
# name: Require
# --
${1:$$(coq-insert-requires)}
$0

View file

@ -0,0 +1,8 @@
# -*- mode: snippet -*-
# key: Axi
# group: propositions
# name: Axiom
# expand-env: ((yas-indent-line 'fixed))
# --
Axiom $1 :
$0.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: Conj
# group: propositions
# name: Conjecture
# --
Conjecture $1 : $0.

View file

@ -0,0 +1,11 @@
# -*- mode: snippet -*-
# key: Cor
# group: propositions
# name: Corollary
# expand-env: ((yas-indent-line 'fixed))
# --
Corollary $1 :
$2.
Proof.
$0
Qed.

View file

@ -0,0 +1,11 @@
# -*- mode: snippet -*-
# key: Exp
# group: propositions
# name: Example
# expand-env: ((yas-indent-line 'fixed))
# --
Example $1 :
$2.
Proof.
$0
Qed.

View file

@ -0,0 +1,11 @@
# -*- mode: snippet -*-
# key: Fact
# group: propositions
# name: Fact
# expand-env: ((yas-indent-line 'fixed))
# --
Fact $1 :
$2.
Proof.
$0
Qed.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: Hypos
# group: propositions
# name: Hypotheses
# --
Hypotheses $1 : $0.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: Hypo
# group: propositions
# name: Hypothesis
# --
Hypothesis $1 : $0.

View file

@ -0,0 +1,11 @@
# -*- mode: snippet -*-
# key: Ins
# group: propositions
# name: Instance
# expand-env: ((yas-indent-line 'fixed))
# --
Instance $1 :
$2.
Proof.
$0
Qed.

View file

@ -0,0 +1,11 @@
# -*- mode: snippet -*-
# key: Lem
# group: propositions
# name: Lemma
# expand-env: ((yas-indent-line 'fixed))
# --
Lemma $1 :
$2.
Proof.
$0
Qed.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: Param
# group: propositions
# name: Parameters
# --
Parameter $1 : $0.

View file

@ -0,0 +1,11 @@
# -*- mode: snippet -*-
# key: Pro
# group: propositions
# name: Proposition
# expand-env: ((yas-indent-line 'fixed))
# --
Proposition $1 :
$2.
Proof.
$0
Qed.

View file

@ -0,0 +1,11 @@
# -*- mode: snippet -*-
# key: Rem
# group: propositions
# name: Remark
# expand-env: ((yas-indent-line 'fixed))
# --
Remark $1 :
$2.
Proof.
$0
Qed.

View file

@ -0,0 +1,11 @@
# -*- mode: snippet -*-
# key: The
# group: propositions
# name: Theorem
# expand-env: ((yas-indent-line 'fixed))
# --
Theorem $1 :
$2.
Proof.
$0
Qed.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: Var
# group: propositions
# name: Variable
# --
Variable $1 : $0.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: Vars
# group: propositions
# name: Variables
# --
Variables $1 : $0.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: case
# group: tactics
# name: case
# --
case ${1:n} as [ | $1' ].$0

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: des
# group: tactics
# name: destruct
# --
destruct $1 as [ $0 ].

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: ind
# group: tactics
# name: induction
# --
induction ${1:n} as [ | $1' IH_$1' ].$0

View file

@ -0,0 +1,7 @@
# -*- mode: snippet -*-
# key: rename
# group: tactics
# name: rename
# --
rename $1 into $2.
$0

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: rwl
# group: tactics
# name: rewrite-left
# --
rewrite <- $0.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: rwr
# group: tactics
# name: rewrite-right
# --
rewrite -> $0.

View file

@ -0,0 +1,6 @@
# -*- mode: snippet -*-
# key: rw
# group: tactics
# name: rewrite
# --
rewrite $0.