branch: elpa/yasnippet-snippets
commit 95b813f758d281fb34ada8410a92b0ac860cdffe
Author: João Diogo Duarte <j...@diogoduarte.pt>
Commit: GitHub <nore...@github.com>
Added easycrypt-mode snippets (#503)
* initial easycrypt mode
* Added emacs files in gitignore
* Added easycrypt snippets
* Removed backup and autosave files
---
.gitignore | 3 +++
snippets/easycrypt-mode/lookup/locate | 7 +++++++
snippets/easycrypt-mode/lookup/print | 7 +++++++
snippets/easycrypt-mode/lookup/search | 7 +++++++
snippets/easycrypt-mode/misc/abbrev | 8 ++++++++
snippets/easycrypt-mode/misc/and1 | 8 ++++++++
snippets/easycrypt-mode/misc/and2 | 8 ++++++++
snippets/easycrypt-mode/misc/comment | 8 ++++++++
snippets/easycrypt-mode/misc/forall | 8 ++++++++
snippets/easycrypt-mode/misc/from | 6 ++++++
snippets/easycrypt-mode/misc/from-jasmin | 7 +++++++
snippets/easycrypt-mode/misc/fun | 8 ++++++++
snippets/easycrypt-mode/misc/ge0 | 8 ++++++++
snippets/easycrypt-mode/misc/geq0 | 6 ++++++
snippets/easycrypt-mode/misc/hint-simplify | 8 ++++++++
snippets/easycrypt-mode/misc/if | 8 ++++++++
snippets/easycrypt-mode/misc/import | 7 +++++++
snippets/easycrypt-mode/misc/let-in | 8 ++++++++
snippets/easycrypt-mode/misc/list | 8 ++++++++
snippets/easycrypt-mode/misc/new-comment | 6 ++++++
snippets/easycrypt-mode/misc/or1 | 8 ++++++++
snippets/easycrypt-mode/misc/or2 | 8 ++++++++
snippets/easycrypt-mode/misc/param | 8 ++++++++
snippets/easycrypt-mode/misc/pred | 7 +++++++
snippets/easycrypt-mode/misc/probability | 8 ++++++++
snippets/easycrypt-mode/misc/probability-mem | 8 ++++++++
snippets/easycrypt-mode/misc/range | 6 ++++++
snippets/easycrypt-mode/misc/range-exclusive | 8 ++++++++
snippets/easycrypt-mode/misc/range-exclusive-inclusive | 8 ++++++++
snippets/easycrypt-mode/misc/range-inclusive | 8 ++++++++
snippets/easycrypt-mode/misc/range-inclusive-exclusive | 8 ++++++++
snippets/easycrypt-mode/misc/require-import | 7 +++++++
snippets/easycrypt-mode/modules/module | 10 ++++++++++
snippets/easycrypt-mode/modules/module-instance | 8 ++++++++
snippets/easycrypt-mode/modules/module-type | 10 ++++++++++
snippets/easycrypt-mode/modules/module-with-params | 8 ++++++++
.../easycrypt-mode/modules/module-with-params-return | 10 ++++++++++
snippets/easycrypt-mode/modules/module-with-return | 10 ++++++++++
snippets/easycrypt-mode/procedures/assign | 8 ++++++++
snippets/easycrypt-mode/procedures/decrement-counter | 8 ++++++++
snippets/easycrypt-mode/procedures/if-else-proc | 12 ++++++++++++
snippets/easycrypt-mode/procedures/if-proc | 10 ++++++++++
snippets/easycrypt-mode/procedures/increment-counter | 8 ++++++++
snippets/easycrypt-mode/procedures/init-var | 8 ++++++++
snippets/easycrypt-mode/procedures/new-var | 8 ++++++++
snippets/easycrypt-mode/procedures/proc | 11 +++++++++++
snippets/easycrypt-mode/procedures/proc-abstract | 8 ++++++++
snippets/easycrypt-mode/procedures/proc-call | 8 ++++++++
snippets/easycrypt-mode/procedures/proc-no-return | 10 ++++++++++
snippets/easycrypt-mode/procedures/sample | 8 ++++++++
snippets/easycrypt-mode/procedures/while-proc | 11 +++++++++++
snippets/easycrypt-mode/propositions/axiom | 7 +++++++
snippets/easycrypt-mode/propositions/axiomatized | 7 +++++++
snippets/easycrypt-mode/propositions/declare | 7 +++++++
snippets/easycrypt-mode/propositions/equiv | 13 +++++++++++++
snippets/easycrypt-mode/propositions/hoare | 13 +++++++++++++
snippets/easycrypt-mode/propositions/lemma | 11 +++++++++++
snippets/easycrypt-mode/propositions/lemma_equality | 11 +++++++++++
snippets/easycrypt-mode/propositions/lemma_equiv | 16 ++++++++++++++++
snippets/easycrypt-mode/propositions/lemma_hoare | 15 +++++++++++++++
snippets/easycrypt-mode/propositions/lemma_islossless | 11 +++++++++++
snippets/easycrypt-mode/propositions/lemma_phoare | 15 +++++++++++++++
snippets/easycrypt-mode/propositions/local | 7 +++++++
snippets/easycrypt-mode/propositions/op-as | 7 +++++++
snippets/easycrypt-mode/propositions/op-axiomatixed | 7 +++++++
snippets/easycrypt-mode/propositions/op-barebones | 7 +++++++
snippets/easycrypt-mode/propositions/op-no-return | 7 +++++++
snippets/easycrypt-mode/propositions/phoare | 14 ++++++++++++++
snippets/easycrypt-mode/propositions/small-lemma | 7 +++++++
snippets/easycrypt-mode/tactics/alias | 8 ++++++++
snippets/easycrypt-mode/tactics/alias-with | 8 ++++++++
snippets/easycrypt-mode/tactics/alias1 | 8 ++++++++
snippets/easycrypt-mode/tactics/alias1-with | 8 ++++++++
snippets/easycrypt-mode/tactics/alias2 | 8 ++++++++
snippets/easycrypt-mode/tactics/alias2-with | 8 ++++++++
snippets/easycrypt-mode/tactics/aliaswith | 6 ++++++
snippets/easycrypt-mode/tactics/aliaswith1 | 6 ++++++
snippets/easycrypt-mode/tactics/aliaswith2 | 6 ++++++
snippets/easycrypt-mode/tactics/apply-args | 8 ++++++++
snippets/easycrypt-mode/tactics/apply-in | 8 ++++++++
snippets/easycrypt-mode/tactics/apply-proof-term | 8 ++++++++
snippets/easycrypt-mode/tactics/async-while | 13 +++++++++++++
snippets/easycrypt-mode/tactics/auto | 7 +++++++
snippets/easycrypt-mode/tactics/auto.yasnippet | 7 +++++++
snippets/easycrypt-mode/tactics/bad-smt | 8 ++++++++
snippets/easycrypt-mode/tactics/byequiv | 8 ++++++++
snippets/easycrypt-mode/tactics/byphoare | 8 ++++++++
snippets/easycrypt-mode/tactics/bypr | 8 ++++++++
snippets/easycrypt-mode/tactics/call | 8 ++++++++
snippets/easycrypt-mode/tactics/call-invar | 8 ++++++++
snippets/easycrypt-mode/tactics/call-invar2 | 8 ++++++++
snippets/easycrypt-mode/tactics/call-invar3 | 8 ++++++++
snippets/easycrypt-mode/tactics/call-true | 8 ++++++++
snippets/easycrypt-mode/tactics/call-true-true | 8 ++++++++
snippets/easycrypt-mode/tactics/call1 | 8 ++++++++
snippets/easycrypt-mode/tactics/call1-invar | 8 ++++++++
snippets/easycrypt-mode/tactics/call1-true | 8 ++++++++
snippets/easycrypt-mode/tactics/call1-true-true | 8 ++++++++
snippets/easycrypt-mode/tactics/call2 | 8 ++++++++
snippets/easycrypt-mode/tactics/call2-invar | 8 ++++++++
snippets/easycrypt-mode/tactics/call2-true | 8 ++++++++
snippets/easycrypt-mode/tactics/call2-true-true | 8 ++++++++
snippets/easycrypt-mode/tactics/case | 8 ++++++++
snippets/easycrypt-mode/tactics/case-move | 8 ++++++++
snippets/easycrypt-mode/tactics/cfold | 8 ++++++++
snippets/easycrypt-mode/tactics/cfold-from-to | 8 ++++++++
snippets/easycrypt-mode/tactics/cfold-from-to1 | 8 ++++++++
snippets/easycrypt-mode/tactics/cfold-from-to2 | 8 ++++++++
snippets/easycrypt-mode/tactics/cfold1 | 8 ++++++++
snippets/easycrypt-mode/tactics/cfold2 | 8 ++++++++
snippets/easycrypt-mode/tactics/cfold_from_to | 6 ++++++
snippets/easycrypt-mode/tactics/cfold_from_to1 | 6 ++++++
snippets/easycrypt-mode/tactics/cfold_from_to2 | 6 ++++++
snippets/easycrypt-mode/tactics/clear | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq-invar | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq-true | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq-true-true | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq1 | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq1-invar | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq1-true | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq1-true-true | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq2 | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq2-invar | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq2-true | 8 ++++++++
snippets/easycrypt-mode/tactics/conseq2-true-true | 8 ++++++++
snippets/easycrypt-mode/tactics/do-n-times | 8 ++++++++
snippets/easycrypt-mode/tactics/do-split | 9 +++++++++
snippets/easycrypt-mode/tactics/dosplit | 7 +++++++
snippets/easycrypt-mode/tactics/ecall | 8 ++++++++
snippets/easycrypt-mode/tactics/ecall-wp | 8 ++++++++
snippets/easycrypt-mode/tactics/elim-proof-term | 8 ++++++++
snippets/easycrypt-mode/tactics/elim-var | 8 ++++++++
snippets/easycrypt-mode/tactics/exists | 8 ++++++++
snippets/easycrypt-mode/tactics/exists-astreix1 | 8 ++++++++
snippets/easycrypt-mode/tactics/exists-astrix | 8 ++++++++
snippets/easycrypt-mode/tactics/first-last | 8 ++++++++
snippets/easycrypt-mode/tactics/first-n-last | 7 +++++++
snippets/easycrypt-mode/tactics/firstn | 8 ++++++++
snippets/easycrypt-mode/tactics/fission | 8 ++++++++
snippets/easycrypt-mode/tactics/fission1 | 8 ++++++++
snippets/easycrypt-mode/tactics/fission2 | 8 ++++++++
snippets/easycrypt-mode/tactics/fusion | 8 ++++++++
snippets/easycrypt-mode/tactics/fusion1 | 8 ++++++++
snippets/easycrypt-mode/tactics/fusion2 | 8 ++++++++
snippets/easycrypt-mode/tactics/have-define | 8 ++++++++
snippets/easycrypt-mode/tactics/have-introduce | 8 ++++++++
snippets/easycrypt-mode/tactics/have-write-left | 8 ++++++++
snippets/easycrypt-mode/tactics/have-write-left-eq | 8 ++++++++
snippets/easycrypt-mode/tactics/have-write-right | 8 ++++++++
snippets/easycrypt-mode/tactics/have-write-right-eq | 8 ++++++++
snippets/easycrypt-mode/tactics/if | 8 ++++++++
snippets/easycrypt-mode/tactics/if1 | 8 ++++++++
snippets/easycrypt-mode/tactics/if2 | 8 ++++++++
snippets/easycrypt-mode/tactics/implies | 7 +++++++
snippets/easycrypt-mode/tactics/implies-brackets | 7 +++++++
snippets/easycrypt-mode/tactics/inline | 6 ++++++
snippets/easycrypt-mode/tactics/inline1 | 8 ++++++++
snippets/easycrypt-mode/tactics/inline2 | 8 ++++++++
snippets/easycrypt-mode/tactics/last | 8 ++++++++
snippets/easycrypt-mode/tactics/last-first | 8 ++++++++
snippets/easycrypt-mode/tactics/last-n-first | 8 ++++++++
snippets/easycrypt-mode/tactics/lastn | 8 ++++++++
snippets/easycrypt-mode/tactics/move-1 | 8 ++++++++
snippets/easycrypt-mode/tactics/move-1m2 | 8 ++++++++
snippets/easycrypt-mode/tactics/move-2 | 8 ++++++++
snippets/easycrypt-mode/tactics/move-from-assumption | 8 ++++++++
snippets/easycrypt-mode/tactics/move-hr | 8 ++++++++
snippets/easycrypt-mode/tactics/move-lemma-args | 8 ++++++++
snippets/easycrypt-mode/tactics/move-to-assumption | 8 ++++++++
snippets/easycrypt-mode/tactics/pose | 8 ++++++++
snippets/easycrypt-mode/tactics/proc-simplify | 8 ++++++++
snippets/easycrypt-mode/tactics/proc-up-to-bad | 8 ++++++++
snippets/easycrypt-mode/tactics/proc-up-to-bad2 | 8 ++++++++
snippets/easycrypt-mode/tactics/rcondf1 | 8 ++++++++
snippets/easycrypt-mode/tactics/rcondf2 | 8 ++++++++
snippets/easycrypt-mode/tactics/rcondt-rl | 6 ++++++
snippets/easycrypt-mode/tactics/rcondt1 | 8 ++++++++
snippets/easycrypt-mode/tactics/rcondt2 | 8 ++++++++
snippets/easycrypt-mode/tactics/repeat-from-to | 8 ++++++++
snippets/easycrypt-mode/tactics/rewrite | 8 ++++++++
snippets/easycrypt-mode/tactics/rewrite-crush | 8 ++++++++
snippets/easycrypt-mode/tactics/rewrite-expand-list | 8 ++++++++
snippets/easycrypt-mode/tactics/rewrite-fun-backwards | 8 ++++++++
snippets/easycrypt-mode/tactics/rewrite-in | 8 ++++++++
.../easycrypt-mode/tactics/rewrite-lemma-forwards-args | 8 ++++++++
snippets/easycrypt-mode/tactics/rewrite-proof-term-in | 8 ++++++++
snippets/easycrypt-mode/tactics/rnd-f | 8 ++++++++
snippets/easycrypt-mode/tactics/rnd-fg | 8 ++++++++
snippets/easycrypt-mode/tactics/rnd1 | 8 ++++++++
snippets/easycrypt-mode/tactics/rnd2 | 7 +++++++
snippets/easycrypt-mode/tactics/seq | 8 ++++++++
snippets/easycrypt-mode/tactics/sim | 8 ++++++++
snippets/easycrypt-mode/tactics/smt | 8 ++++++++
snippets/easycrypt-mode/tactics/splitwhile | 8 ++++++++
snippets/easycrypt-mode/tactics/splitwhile1 | 8 ++++++++
snippets/easycrypt-mode/tactics/splitwhile2 | 8 ++++++++
snippets/easycrypt-mode/tactics/transitivity | 10 ++++++++++
snippets/easycrypt-mode/tactics/transitivity-code | 10 ++++++++++
snippets/easycrypt-mode/tactics/unroll-equiv | 8 ++++++++
snippets/easycrypt-mode/tactics/unroll-while | 8 ++++++++
snippets/easycrypt-mode/tactics/while | 10 ++++++++++
snippets/easycrypt-mode/tactics/while-true | 8 ++++++++
snippets/easycrypt-mode/tactics/while1 | 8 ++++++++
snippets/easycrypt-mode/tactics/while2 | 7 +++++++
snippets/easycrypt-mode/theories/abstract-theory | 11 +++++++++++
snippets/easycrypt-mode/theories/clone-as | 8 ++++++++
snippets/easycrypt-mode/theories/clone-as-with | 8 ++++++++
snippets/easycrypt-mode/theories/clone-import | 8 ++++++++
snippets/easycrypt-mode/theories/clone-include | 8 ++++++++
snippets/easycrypt-mode/theories/clone-no-with | 6 ++++++
snippets/easycrypt-mode/theories/rename-as | 8 ++++++++
snippets/easycrypt-mode/theories/section | 10 ++++++++++
snippets/easycrypt-mode/theories/theory | 11 +++++++++++
snippets/easycrypt-mode/theories/type | 8 ++++++++
snippets/easycrypt-mode/theories/with | 8 ++++++++
216 files changed, 1762 insertions(+)
diff --git a/.gitignore b/.gitignore
index 02ac900f2e..8540a89c7b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,3 +3,6 @@
/report/.nrepl-port
/.clj-kondo/
/.lsp/
+*~
+\#*\#
+.\#*
diff --git a/snippets/easycrypt-mode/lookup/locate
b/snippets/easycrypt-mode/lookup/locate
new file mode 100644
index 0000000000..3115f2d47c
--- /dev/null
+++ b/snippets/easycrypt-mode/lookup/locate
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: L
+# group: lookup
+# name: locate
+# expand-env: ((yas-indent-line 'fixed))
+# --
+locate $1.
diff --git a/snippets/easycrypt-mode/lookup/print
b/snippets/easycrypt-mode/lookup/print
new file mode 100644
index 0000000000..b0b3490ba1
--- /dev/null
+++ b/snippets/easycrypt-mode/lookup/print
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: P
+# group: lookup
+# name: print
+# expand-env: ((yas-indent-line 'fixed))
+# --
+print $1.
diff --git a/snippets/easycrypt-mode/lookup/search
b/snippets/easycrypt-mode/lookup/search
new file mode 100644
index 0000000000..6f76478546
--- /dev/null
+++ b/snippets/easycrypt-mode/lookup/search
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: S
+# group: lookup
+# name: search
+# expand-env: ((yas-indent-line 'fixed))
+# --
+search $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/abbrev
b/snippets/easycrypt-mode/misc/abbrev
new file mode 100644
index 0000000000..9a43002172
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/abbrev
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: abbrev
+# key: abbrev
+# expand-env: ((yas-indent-line 'fixed))
+# --
+abbrev $1 = $2.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/and1
b/snippets/easycrypt-mode/misc/and1
new file mode 100644
index 0000000000..50a04363ba
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/and1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: and1
+# key: and1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 /\ $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/and2
b/snippets/easycrypt-mode/misc/and2
new file mode 100644
index 0000000000..1f6f29d296
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/and2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: and2
+# key: and2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 && $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/comment
b/snippets/easycrypt-mode/misc/comment
new file mode 100644
index 0000000000..5ab8f8afb7
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/comment
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: comment
+# key: comment
+# expand-env: ((yas-indent-line 'fixed))
+# --
+(* $1 *)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/forall
b/snippets/easycrypt-mode/misc/forall
new file mode 100644
index 0000000000..308d9def85
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/forall
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: forall
+# key: forall
+# expand-env: ((yas-indent-line 'fixed))
+# --
+forall ($1: $2), $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/from
b/snippets/easycrypt-mode/misc/from
new file mode 100644
index 0000000000..c905177bda
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/from
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: from
+# group: misc
+# name: from
+# --
+from $1 require import $2.
diff --git a/snippets/easycrypt-mode/misc/from-jasmin
b/snippets/easycrypt-mode/misc/from-jasmin
new file mode 100644
index 0000000000..b15234d4a3
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/from-jasmin
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: from-jasmin
+# group: misc
+# name: from-jasmin
+# expand-env: ((yas-indent-line 'fixed))
+# --
+from Jasmin require import $1.
diff --git a/snippets/easycrypt-mode/misc/fun b/snippets/easycrypt-mode/misc/fun
new file mode 100644
index 0000000000..13d660afc4
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/fun
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: fun
+# key: fun
+# expand-env: ((yas-indent-line 'fixed))
+# --
+fun ($1) => $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/ge0 b/snippets/easycrypt-mode/misc/ge0
new file mode 100644
index 0000000000..568d53ee0f
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/ge0
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: ge0
+# key: ge0
+# expand-env: ((yas-indent-line 'fixed))
+# --
+0 <= $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/geq0
b/snippets/easycrypt-mode/misc/geq0
new file mode 100644
index 0000000000..68a2476449
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/geq0
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: ge0
+# key: ge0
+# --
+0 <= $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/hint-simplify
b/snippets/easycrypt-mode/misc/hint-simplify
new file mode 100644
index 0000000000..42d0783922
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/hint-simplify
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: hint-simplify
+# key: hint
+# expand-env: ((yas-indent-line 'fixed))
+# --
+hint simplify $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/if b/snippets/easycrypt-mode/misc/if
new file mode 100644
index 0000000000..07ff756e2c
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/if
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: if
+# key: if
+# expand-env: ((yas-indent-line 'fixed))
+# --
+if $1 then $2 else $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/import
b/snippets/easycrypt-mode/misc/import
new file mode 100644
index 0000000000..3e6e466fb8
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/import
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: import
+# group: misc
+# name: import
+# expand-env: ((yas-indent-line 'fixed))
+# --
+import $1.
diff --git a/snippets/easycrypt-mode/misc/let-in
b/snippets/easycrypt-mode/misc/let-in
new file mode 100644
index 0000000000..efb9682324
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/let-in
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: let-in
+# key: let-in
+# expand-env: ((yas-indent-line 'fixed))
+# --
+let $1 in $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/list
b/snippets/easycrypt-mode/misc/list
new file mode 100644
index 0000000000..6f40a8bd6a
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/list
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: list
+# key: list
+# expand-env: ((yas-indent-line 'fixed))
+# --
+[$1 ; $2]
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/new-comment
b/snippets/easycrypt-mode/misc/new-comment
new file mode 100644
index 0000000000..3d6a9c4233
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/new-comment
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: new-comment
+# key: new-comment
+# --
+(* $1 *)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/or1 b/snippets/easycrypt-mode/misc/or1
new file mode 100644
index 0000000000..ca782198fc
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/or1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: or1
+# key: or1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 \/ $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/or2 b/snippets/easycrypt-mode/misc/or2
new file mode 100644
index 0000000000..02877126d8
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/or2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: or2
+# key: or2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 || $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/param
b/snippets/easycrypt-mode/misc/param
new file mode 100644
index 0000000000..5976e96259
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/param
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: param
+# key: param
+# expand-env: ((yas-indent-line 'fixed))
+# --
+($1 : $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/pred
b/snippets/easycrypt-mode/misc/pred
new file mode 100644
index 0000000000..ac00ed83c8
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/pred
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: pred
+# group: misc
+# name: pred
+# expand-env: ((yas-indent-line 'fixed))
+# --
+pred $1 = $2.
diff --git a/snippets/easycrypt-mode/misc/probability
b/snippets/easycrypt-mode/misc/probability
new file mode 100644
index 0000000000..23383bb57a
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/probability
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: probability
+# key: probability
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Pr[$1]
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/probability-mem
b/snippets/easycrypt-mode/misc/probability-mem
new file mode 100644
index 0000000000..8eb21d3a02
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/probability-mem
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: probability-memory
+# key: probability-memory
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Pr[$1 @ &$2 : $3]
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/range
b/snippets/easycrypt-mode/misc/range
new file mode 100644
index 0000000000..4084dc8c02
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/range
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: range
+# key: range
+# --
+$1 <= $2 <= $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/range-exclusive
b/snippets/easycrypt-mode/misc/range-exclusive
new file mode 100644
index 0000000000..d92390e7a0
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/range-exclusive
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: range-exclusive
+# key: range-exclusive
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 < $2 < $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/range-exclusive-inclusive
b/snippets/easycrypt-mode/misc/range-exclusive-inclusive
new file mode 100644
index 0000000000..267cdb934e
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/range-exclusive-inclusive
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: range-exclusive-inclusive
+# key: range-exclusive-inclusive
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 < $2 <= $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/range-inclusive
b/snippets/easycrypt-mode/misc/range-inclusive
new file mode 100644
index 0000000000..03774eda01
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/range-inclusive
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: range-inclusive
+# key: range-inclusive
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 <= $2 <= $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/range-inclusive-exclusive
b/snippets/easycrypt-mode/misc/range-inclusive-exclusive
new file mode 100644
index 0000000000..0618a1bd56
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/range-inclusive-exclusive
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: range-inclusive-exclusive
+# key: range-inclusive-exclusive
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 <= $2 < $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/misc/require-import
b/snippets/easycrypt-mode/misc/require-import
new file mode 100644
index 0000000000..99ac5d0efd
--- /dev/null
+++ b/snippets/easycrypt-mode/misc/require-import
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: require-import
+# group: misc
+# name: require-import
+# expand-env: ((yas-indent-line 'fixed))
+# --
+require import $1.
diff --git a/snippets/easycrypt-mode/modules/module
b/snippets/easycrypt-mode/modules/module
new file mode 100644
index 0000000000..e6e768ece0
--- /dev/null
+++ b/snippets/easycrypt-mode/modules/module
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: modules
+# name: module
+# key: module
+# expand-env: ((yas-indent-line 'fixed))
+# --
+module $1 = {
+
+}.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/modules/module-instance
b/snippets/easycrypt-mode/modules/module-instance
new file mode 100644
index 0000000000..2c24e55d1a
--- /dev/null
+++ b/snippets/easycrypt-mode/modules/module-instance
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: modules
+# name: module-instance
+# key: module-instance
+# expand-env: ((yas-indent-line 'fixed))
+# --
+module $1 = $2($3).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/modules/module-type
b/snippets/easycrypt-mode/modules/module-type
new file mode 100644
index 0000000000..b88edff227
--- /dev/null
+++ b/snippets/easycrypt-mode/modules/module-type
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: modules
+# name: module-type
+# key: module-type
+# expand-env: ((yas-indent-line 'fixed))
+# --
+module type $1 = {
+
+}.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/modules/module-with-params
b/snippets/easycrypt-mode/modules/module-with-params
new file mode 100644
index 0000000000..5e84cbf878
--- /dev/null
+++ b/snippets/easycrypt-mode/modules/module-with-params
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: module-with-params
+# key: module-with-params
+# --
+module $1 ($2: $3) : $4 {
+
+}.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/modules/module-with-params-return
b/snippets/easycrypt-mode/modules/module-with-params-return
new file mode 100644
index 0000000000..f70c69cd28
--- /dev/null
+++ b/snippets/easycrypt-mode/modules/module-with-params-return
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: modules
+# name: module-with-params-return
+# key: module-with-params-return
+# expand-env: ((yas-indent-line 'fixed))
+# --
+module $1 ($2: $3) : $4 {
+
+}.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/modules/module-with-return
b/snippets/easycrypt-mode/modules/module-with-return
new file mode 100644
index 0000000000..cb6d8461c5
--- /dev/null
+++ b/snippets/easycrypt-mode/modules/module-with-return
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: modules
+# name: module-with-return
+# key: module-with-return
+# expand-env: ((yas-indent-line 'fixed))
+# --
+module $1 : $2 = {
+
+}.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/assign
b/snippets/easycrypt-mode/procedures/assign
new file mode 100644
index 0000000000..ca3166968a
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/assign
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: assign
+# key: assign
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 <- $2;
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/decrement-counter
b/snippets/easycrypt-mode/procedures/decrement-counter
new file mode 100644
index 0000000000..3f9477903f
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/decrement-counter
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: decrement-counter
+# key: decrement-counter
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 <- $1 - 1;
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/if-else-proc
b/snippets/easycrypt-mode/procedures/if-else-proc
new file mode 100644
index 0000000000..d4914c2284
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/if-else-proc
@@ -0,0 +1,12 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: if-else-proc
+# key: if-else-proc
+# expand-env: ((yas-indent-line 'fixed))
+# --
+if ($1){
+
+ } else {
+
+}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/if-proc
b/snippets/easycrypt-mode/procedures/if-proc
new file mode 100644
index 0000000000..3e6c800956
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/if-proc
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: if
+# key: if
+# expand-env: ((yas-indent-line 'fixed))
+# --
+if ($1) {
+
+}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/increment-counter
b/snippets/easycrypt-mode/procedures/increment-counter
new file mode 100644
index 0000000000..2909e5b5a5
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/increment-counter
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: increment-counter
+# key: increment-counter
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 <- $1 + 1;
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/init-var
b/snippets/easycrypt-mode/procedures/init-var
new file mode 100644
index 0000000000..84cbff0cdb
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/init-var
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: init-var
+# key: init-var
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 <- witness;
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/new-var
b/snippets/easycrypt-mode/procedures/new-var
new file mode 100644
index 0000000000..409eb7d7cb
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/new-var
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: new-var
+# key: new-var
+# expand-env: ((yas-indent-line 'fixed))
+# --
+var $1 : $2;
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/proc
b/snippets/easycrypt-mode/procedures/proc
new file mode 100644
index 0000000000..3d1c561ef6
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/proc
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: proc
+# key: proc
+# expand-env: ((yas-indent-line 'fixed))
+# --
+proc $1($2 : $3) : $4 = {
+
+ return $5;
+}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/proc-abstract
b/snippets/easycrypt-mode/procedures/proc-abstract
new file mode 100644
index 0000000000..4824f3c439
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/proc-abstract
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: proc-abstract
+# key: proc-abstract
+# expand-env: ((yas-indent-line 'fixed))
+# --
+proc $1($2: $3) : $4
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/proc-call
b/snippets/easycrypt-mode/procedures/proc-call
new file mode 100644
index 0000000000..2a3ef70f1a
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/proc-call
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: proc-call
+# key: proc-call
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 <@ $2;
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/proc-no-return
b/snippets/easycrypt-mode/procedures/proc-no-return
new file mode 100644
index 0000000000..c6a22de091
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/proc-no-return
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: proc-no-return
+# key: proc-no-return
+# expand-env: ((yas-indent-line 'fixed))
+# --
+proc $1 ($2: $3) = {
+
+}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/sample
b/snippets/easycrypt-mode/procedures/sample
new file mode 100644
index 0000000000..514879ef73
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/sample
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: sample
+# key: sample
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1 <$ $2;
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/procedures/while-proc
b/snippets/easycrypt-mode/procedures/while-proc
new file mode 100644
index 0000000000..b68bf57810
--- /dev/null
+++ b/snippets/easycrypt-mode/procedures/while-proc
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: procedures
+# name: while-proc
+# key: while-proc
+# expand-env: ((yas-indent-line 'fixed))
+# --
+while ($1)
+{
+
+}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/propositions/axiom
b/snippets/easycrypt-mode/propositions/axiom
new file mode 100644
index 0000000000..0a144149e5
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/axiom
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: axiom
+# group: propositions
+# name: axiom
+# expand-env: ((yas-indent-line 'fixed))
+# --
+axiom $1 : $2.
diff --git a/snippets/easycrypt-mode/propositions/axiomatized
b/snippets/easycrypt-mode/propositions/axiomatized
new file mode 100644
index 0000000000..14e9a90483
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/axiomatized
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: axiomatized
+# key: axiomatized
+# expand-env: ((yas-indent-line 'fixed))
+# --
+axiomatized by $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/propositions/declare
b/snippets/easycrypt-mode/propositions/declare
new file mode 100644
index 0000000000..a1d684ea6b
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/declare
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: declare
+# group: propositions
+# name: declare
+# expand-env: ((yas-indent-line 'fixed))
+# --
+declare $1
diff --git a/snippets/easycrypt-mode/propositions/equiv
b/snippets/easycrypt-mode/propositions/equiv
new file mode 100644
index 0000000000..d61ffe2769
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/equiv
@@ -0,0 +1,13 @@
+# -*- mode: snippet -*-
+# key: equiv
+# group: propositions
+# name: equiv
+# expand-env: ((yas-indent-line 'fixed))
+# --
+equiv $1 : $2 ~ $3 :
+ $4
+ ==>
+ $5 .
+proof.
+
+qed.
diff --git a/snippets/easycrypt-mode/propositions/hoare
b/snippets/easycrypt-mode/propositions/hoare
new file mode 100644
index 0000000000..4ba84f48e0
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/hoare
@@ -0,0 +1,13 @@
+# -*- mode: snippet -*-
+# key: hoare
+# group: propositions
+# name: hoare
+# expand-env: ((yas-indent-line 'fixed))
+# --
+hoare $1 : $2 :
+ $3
+ ==>
+ $4.
+proof.
+
+qed.
diff --git a/snippets/easycrypt-mode/propositions/lemma
b/snippets/easycrypt-mode/propositions/lemma
new file mode 100644
index 0000000000..1986d59f24
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/lemma
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: lemma
+# group: propositions
+# name: lemma
+# expand-env: ((yas-indent-line 'fixed))
+# --
+lemma $1 :
+ $2.
+proof.
+
+qed.
diff --git a/snippets/easycrypt-mode/propositions/lemma_equality
b/snippets/easycrypt-mode/propositions/lemma_equality
new file mode 100644
index 0000000000..10be8aaa4b
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/lemma_equality
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: lemma-equality
+# key: lemma-equality
+# expand-env: ((yas-indent-line 'fixed))
+# --
+lemma $1 :
+ ($2) = ($3).
+proof.
+$4
+qed.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/propositions/lemma_equiv
b/snippets/easycrypt-mode/propositions/lemma_equiv
new file mode 100644
index 0000000000..6cb526913d
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/lemma_equiv
@@ -0,0 +1,16 @@
+# -*- mode: snippet -*-
+# key: lemma-equiv
+# group: propositions
+# name: lemma-equiv
+# expand-env: ((yas-indent-line 'fixed))
+# --
+lemma $1 :
+ equiv [
+ $2 ~ $3
+ $4
+ ==>
+ $5
+ ].
+proof.
+
+qed.
diff --git a/snippets/easycrypt-mode/propositions/lemma_hoare
b/snippets/easycrypt-mode/propositions/lemma_hoare
new file mode 100644
index 0000000000..5c2d2621bb
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/lemma_hoare
@@ -0,0 +1,15 @@
+# -*- mode: snippet -*-
+# key: lemma-hoare
+# group: propositions
+# name: lemma-hoare
+# expand-env: ((yas-indent-line 'fixed))
+# --
+lemma $1 :
+ hoare [
+ $2
+ ==>
+ $3
+ ].
+proof.
+
+qed.
diff --git a/snippets/easycrypt-mode/propositions/lemma_islossless
b/snippets/easycrypt-mode/propositions/lemma_islossless
new file mode 100644
index 0000000000..15d9abb377
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/lemma_islossless
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: lemma-islossless
+# group: propositions
+# name: lemma-islossless
+# expand-env: ((yas-indent-line 'fixed))
+# --
+lemma $1 : islossless
+ $2.
+proof.
+
+qed.
diff --git a/snippets/easycrypt-mode/propositions/lemma_phoare
b/snippets/easycrypt-mode/propositions/lemma_phoare
new file mode 100644
index 0000000000..2d41e65b71
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/lemma_phoare
@@ -0,0 +1,15 @@
+# -*- mode: snippet -*-
+# key: lemma-phoare
+# group: propositions
+# name: lemma-phoare
+# expand-env: ((yas-indent-line 'fixed))
+# --
+lemma $1 :
+ phoare [
+ $2
+ ==>
+ $3
+ ] = 1%r.
+proof.
+
+qed.
diff --git a/snippets/easycrypt-mode/propositions/local
b/snippets/easycrypt-mode/propositions/local
new file mode 100644
index 0000000000..8dc4f14e9f
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/local
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: local
+# group: propositions
+# name: local
+# expand-env: ((yas-indent-line 'fixed))
+# --
+local $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/propositions/op-as
b/snippets/easycrypt-mode/propositions/op-as
new file mode 100644
index 0000000000..dd46184ad1
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/op-as
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: op-as
+# key: op-as
+# expand-env: ((yas-indent-line 'fixed))
+# --
+op $1 : {$2 | $3} as $4.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/propositions/op-axiomatixed
b/snippets/easycrypt-mode/propositions/op-axiomatixed
new file mode 100644
index 0000000000..13d80f3abd
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/op-axiomatixed
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: op-axiomatized
+# key: op-axiomatized
+# expand-env: ((yas-indent-line 'fixed))
+# --
+op $1 = $2 axiomatized by $3.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/propositions/op-barebones
b/snippets/easycrypt-mode/propositions/op-barebones
new file mode 100644
index 0000000000..962138c1d6
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/op-barebones
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: op-barebones
+# key: op-barebones
+# expand-env: ((yas-indent-line 'fixed))
+# --
+op $1 = $2.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/propositions/op-no-return
b/snippets/easycrypt-mode/propositions/op-no-return
new file mode 100644
index 0000000000..754eb62f21
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/op-no-return
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: op-no-return
+# key: op-no-return
+# expand-env: ((yas-indent-line 'fixed))
+# --
+op $1 ($2: $3) = $4.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/propositions/phoare
b/snippets/easycrypt-mode/propositions/phoare
new file mode 100644
index 0000000000..a0280c964c
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/phoare
@@ -0,0 +1,14 @@
+# -*- mode: snippet -*-
+# key: phoare
+# group: propositions
+# name: phoare
+# expand-env: ((yas-indent-line 'fixed))
+# --
+phoare :
+ [ $1
+ ==>
+ $2
+ ] = 1%r.
+proof.
+
+qed.
diff --git a/snippets/easycrypt-mode/propositions/small-lemma
b/snippets/easycrypt-mode/propositions/small-lemma
new file mode 100644
index 0000000000..285ebec48e
--- /dev/null
+++ b/snippets/easycrypt-mode/propositions/small-lemma
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: small-lemma
+# key: small-lemma
+# expand-env: ((yas-indent-line 'fixed))
+# --
+lemma $1 : $2 by $3.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/alias
b/snippets/easycrypt-mode/tactics/alias
new file mode 100644
index 0000000000..6ebd7c34c3
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/alias
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: alias
+# key: alias
+# expand-env: ((yas-indent-line 'fixed))
+# --
+alias $1 $2 = $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/alias-with
b/snippets/easycrypt-mode/tactics/alias-with
new file mode 100644
index 0000000000..30b9d64277
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/alias-with
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: alias-with
+# key: alias-with
+# expand-env: ((yas-indent-line 'fixed))
+# --
+alias $1 with $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/alias1
b/snippets/easycrypt-mode/tactics/alias1
new file mode 100644
index 0000000000..62b2bee360
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/alias1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: alias1
+# key: alias1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+alias{1} $1 $2 = $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/alias1-with
b/snippets/easycrypt-mode/tactics/alias1-with
new file mode 100644
index 0000000000..c2b231b76b
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/alias1-with
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: alias-with1
+# key: alias-with1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+alias{1} $1 with $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/alias2
b/snippets/easycrypt-mode/tactics/alias2
new file mode 100644
index 0000000000..9ba63bf6b6
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/alias2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: alias2
+# key: alias2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+alias{2} $1 $2 = $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/alias2-with
b/snippets/easycrypt-mode/tactics/alias2-with
new file mode 100644
index 0000000000..519a13b17c
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/alias2-with
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: alias-with2
+# key: alias-with2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+alias{2} $1 with $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/aliaswith
b/snippets/easycrypt-mode/tactics/aliaswith
new file mode 100644
index 0000000000..3c8e037096
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/aliaswith
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: aliaswith
+# key: aliaswith
+# --
+alias $1 with $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/aliaswith1
b/snippets/easycrypt-mode/tactics/aliaswith1
new file mode 100644
index 0000000000..dd1e3a40ab
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/aliaswith1
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: aliaswith1
+# key: aliaswith1
+# --
+alias{1} $1 with $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/aliaswith2
b/snippets/easycrypt-mode/tactics/aliaswith2
new file mode 100644
index 0000000000..f2e4152445
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/aliaswith2
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: aliaswith2
+# key: aliaswith2
+# --
+alias{2} $1 with $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/apply-args
b/snippets/easycrypt-mode/tactics/apply-args
new file mode 100644
index 0000000000..9896845955
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/apply-args
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: apply-args
+# key: apply-args
+# expand-env: ((yas-indent-line 'fixed))
+# --
+apply ($1 $2).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/apply-in
b/snippets/easycrypt-mode/tactics/apply-in
new file mode 100644
index 0000000000..328e38b4d6
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/apply-in
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: apply-in
+# key: apply-in
+# expand-env: ((yas-indent-line 'fixed))
+# --
+apply $1 in $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/apply-proof-term
b/snippets/easycrypt-mode/tactics/apply-proof-term
new file mode 100644
index 0000000000..54fb0e6790
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/apply-proof-term
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: apply-proof-term
+# key: apply-proof-term
+# expand-env: ((yas-indent-line 'fixed))
+# --
+apply /$1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/async-while
b/snippets/easycrypt-mode/tactics/async-while
new file mode 100644
index 0000000000..e37b8b35ee
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/async-while
@@ -0,0 +1,13 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: async-while
+# key: async-while
+# expand-env: ((yas-indent-line 'fixed))
+# --
+async while
+ [ (fun r => $1), ($2) ]
+ [ (fun r => $3), ($2) ]
+ ($4) ($5)
+ :
+ ($6).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/auto
b/snippets/easycrypt-mode/tactics/auto
new file mode 100644
index 0000000000..129e8f5700
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/auto
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: auto
+# group: tactics
+# name: auto
+# expand-env: ((yas-indent-line 'fixed))
+# --
+auto => />.
diff --git a/snippets/easycrypt-mode/tactics/auto.yasnippet
b/snippets/easycrypt-mode/tactics/auto.yasnippet
new file mode 100644
index 0000000000..129e8f5700
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/auto.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: auto
+# group: tactics
+# name: auto
+# expand-env: ((yas-indent-line 'fixed))
+# --
+auto => />.
diff --git a/snippets/easycrypt-mode/tactics/bad-smt
b/snippets/easycrypt-mode/tactics/bad-smt
new file mode 100644
index 0000000000..86d9f11486
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/bad-smt
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: bad-smt
+# key: bad-smt
+# expand-env: ((yas-indent-line 'fixed))
+# --
+smt.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/byequiv
b/snippets/easycrypt-mode/tactics/byequiv
new file mode 100644
index 0000000000..fd87d692ee
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/byequiv
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: byequiv
+# key: byequiv
+# expand-env: ((yas-indent-line 'fixed))
+# --
+byequiv (_ : $1 ==> $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/byphoare
b/snippets/easycrypt-mode/tactics/byphoare
new file mode 100644
index 0000000000..dc81c21e41
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/byphoare
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: byphoare
+# key: nyphoare
+# expand-env: ((yas-indent-line 'fixed))
+# --
+byphoare (_ : $1 ==> $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/bypr
b/snippets/easycrypt-mode/tactics/bypr
new file mode 100644
index 0000000000..82804e74e3
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/bypr
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: bypr
+# key: bypr
+# expand-env: ((yas-indent-line 'fixed))
+# --
+bypr ($1){1} ($2){2}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call
b/snippets/easycrypt-mode/tactics/call
new file mode 100644
index 0000000000..61caf5ae45
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call
+# key: call
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call (_ : $1 ==> $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call-invar
b/snippets/easycrypt-mode/tactics/call-invar
new file mode 100644
index 0000000000..8bb870b845
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call-invar
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call-invar
+# key: call-invar
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call (_: $1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call-invar2
b/snippets/easycrypt-mode/tactics/call-invar2
new file mode 100644
index 0000000000..1a1f3af891
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call-invar2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call-invar2
+# key: call-invar2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call (_: $1, $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call-invar3
b/snippets/easycrypt-mode/tactics/call-invar3
new file mode 100644
index 0000000000..d850a2cf71
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call-invar3
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call-invar3
+# key: call-invar3
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call (_: $1, $2, $3)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call-true
b/snippets/easycrypt-mode/tactics/call-true
new file mode 100644
index 0000000000..111dc91cfe
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call-true
+# key: call-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call (_: true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call-true-true
b/snippets/easycrypt-mode/tactics/call-true-true
new file mode 100644
index 0000000000..d1bd0f162b
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call-true-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call-true-true
+# key: call-true-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call(_: true ==> true).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call1
b/snippets/easycrypt-mode/tactics/call1
new file mode 100644
index 0000000000..a227a43bec
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call1
+# key: call1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call{1} (_ : $1 ==> $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call1-invar
b/snippets/easycrypt-mode/tactics/call1-invar
new file mode 100644
index 0000000000..6e2823687e
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call1-invar
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call1-invar
+# key: call1-invar
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call{1} ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call1-true
b/snippets/easycrypt-mode/tactics/call1-true
new file mode 100644
index 0000000000..87d3bcd96c
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call1-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call1-true
+# key: call1-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call{1} (_ : true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call1-true-true
b/snippets/easycrypt-mode/tactics/call1-true-true
new file mode 100644
index 0000000000..6edc478bb4
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call1-true-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call1-true-true
+# key: call1-true-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call{1} (_ : true ==> true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call2
b/snippets/easycrypt-mode/tactics/call2
new file mode 100644
index 0000000000..94bbe7f038
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call2
+# key: call2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call{2} (_ : $1 ==> $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call2-invar
b/snippets/easycrypt-mode/tactics/call2-invar
new file mode 100644
index 0000000000..cffbc40478
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call2-invar
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call2-invar
+# key: call2-invar
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call{2} ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call2-true
b/snippets/easycrypt-mode/tactics/call2-true
new file mode 100644
index 0000000000..f25c34e141
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call2-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call2-true
+# key: call2-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call{2} (_ : true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/call2-true-true
b/snippets/easycrypt-mode/tactics/call2-true-true
new file mode 100644
index 0000000000..5ba866e6cb
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/call2-true-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: call2-true-true
+# key: call2-true-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+call{2} (_ : true ==> true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/case
b/snippets/easycrypt-mode/tactics/case
new file mode 100644
index 0000000000..d994135ac3
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/case
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: case
+# key: case
+# expand-env: ((yas-indent-line 'fixed))
+# --
+case: ($1{1})
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/case-move
b/snippets/easycrypt-mode/tactics/case-move
new file mode 100644
index 0000000000..7870ec7a0f
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/case-move
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: case-move
+# key: case-move
+# expand-env: ((yas-indent-line 'fixed))
+# --
+case: ($1{1}) => $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold
b/snippets/easycrypt-mode/tactics/cfold
new file mode 100644
index 0000000000..462536ed47
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: cfold
+# key: cfold
+# expand-env: ((yas-indent-line 'fixed))
+# --
+cfold $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold-from-to
b/snippets/easycrypt-mode/tactics/cfold-from-to
new file mode 100644
index 0000000000..6e35b33d19
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold-from-to
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: cfold-from-to
+# key: cfold-from-to
+# expand-env: ((yas-indent-line 'fixed))
+# --
+cfold $1 ! $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold-from-to1
b/snippets/easycrypt-mode/tactics/cfold-from-to1
new file mode 100644
index 0000000000..0dd4d704a8
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold-from-to1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: cfold-from-to1
+# key: cfold-from-to1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+cfold{1} $1 ! $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold-from-to2
b/snippets/easycrypt-mode/tactics/cfold-from-to2
new file mode 100644
index 0000000000..b84d070eb4
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold-from-to2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: cfold-from-to2
+# key: cfold-from-to2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+cfold{2} $1 ! $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold1
b/snippets/easycrypt-mode/tactics/cfold1
new file mode 100644
index 0000000000..75c801ec31
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: cfold1
+# key: cfold1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+cfold{1} $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold2
b/snippets/easycrypt-mode/tactics/cfold2
new file mode 100644
index 0000000000..d3a4ccba35
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: cfold2
+# key: cfold2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+cfold{2} $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold_from_to
b/snippets/easycrypt-mode/tactics/cfold_from_to
new file mode 100644
index 0000000000..68a2b5599d
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold_from_to
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: cfold_from_to
+# key: cfold_from_to
+# --
+cfold $1 ! $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold_from_to1
b/snippets/easycrypt-mode/tactics/cfold_from_to1
new file mode 100644
index 0000000000..e9f6221f1d
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold_from_to1
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: cfold_from_to1
+# key: cfold_from_to1
+# --
+cfold{1} $1 ! $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/cfold_from_to2
b/snippets/easycrypt-mode/tactics/cfold_from_to2
new file mode 100644
index 0000000000..2ba6ab6d37
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/cfold_from_to2
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: cfold_from_to2
+# key: cfold_from_to2
+# --
+cfold{2} $1 ! $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/clear
b/snippets/easycrypt-mode/tactics/clear
new file mode 100644
index 0000000000..aef333dee7
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/clear
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: clear
+# key: clear
+# expand-env: ((yas-indent-line 'fixed))
+# --
+clear $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq
b/snippets/easycrypt-mode/tactics/conseq
new file mode 100644
index 0000000000..f385efdafd
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq
+# key: conseq
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq (_ : $1 ==> $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq-invar
b/snippets/easycrypt-mode/tactics/conseq-invar
new file mode 100644
index 0000000000..f2d5d60005
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq-invar
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq-invar
+# key: conseq-invar
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq (_ : $1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq-true
b/snippets/easycrypt-mode/tactics/conseq-true
new file mode 100644
index 0000000000..8397f5cc51
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq-true
+# key: conseq-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq (_: _ ==> true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq-true-true
b/snippets/easycrypt-mode/tactics/conseq-true-true
new file mode 100644
index 0000000000..cd38e952a9
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq-true-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq-true-true
+# key: conseq-true-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq (_: true ==> true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq1
b/snippets/easycrypt-mode/tactics/conseq1
new file mode 100644
index 0000000000..880e2fa68f
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq1
+# key: conseq1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq{1} (_ : $1 ==> $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq1-invar
b/snippets/easycrypt-mode/tactics/conseq1-invar
new file mode 100644
index 0000000000..e02ad18a62
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq1-invar
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq1-invar
+# key: conseq1-invar
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq{1} ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq1-true
b/snippets/easycrypt-mode/tactics/conseq1-true
new file mode 100644
index 0000000000..cd4c655818
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq1-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq1-true
+# key: conseq1-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq{1} (_ : true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq1-true-true
b/snippets/easycrypt-mode/tactics/conseq1-true-true
new file mode 100644
index 0000000000..a7dcd801e8
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq1-true-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq1-true-true
+# key: conseq1-true-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq{1} (_ : true ==> true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq2
b/snippets/easycrypt-mode/tactics/conseq2
new file mode 100644
index 0000000000..bfcc44d3c5
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq2
+# key: conseq2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq{2} (_ : $1 ==> $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq2-invar
b/snippets/easycrypt-mode/tactics/conseq2-invar
new file mode 100644
index 0000000000..ffc44e7127
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq2-invar
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq2-invar
+# key: conseq2-invar
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq{2} ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq2-true
b/snippets/easycrypt-mode/tactics/conseq2-true
new file mode 100644
index 0000000000..c541f83c86
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq2-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq2-true
+# key: conseq2-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq{2} (_ : true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/conseq2-true-true
b/snippets/easycrypt-mode/tactics/conseq2-true-true
new file mode 100644
index 0000000000..0da984e22c
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/conseq2-true-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: conseq2-true-true
+# key: conseq2-true-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+conseq{2} (_ : true ==> true)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/do-n-times
b/snippets/easycrypt-mode/tactics/do-n-times
new file mode 100644
index 0000000000..2bb626c29f
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/do-n-times
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: do-n-times
+# key: do-n-times
+# expand-env: ((yas-indent-line 'fixed))
+# --
+do $1! ($2).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/do-split
b/snippets/easycrypt-mode/tactics/do-split
new file mode 100644
index 0000000000..27ab47c957
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/do-split
@@ -0,0 +1,9 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: dosplit
+# key: dosplit
+# expand-env: ((yas-indent-line 'fixed))
+# --
+do split.
+ + $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/dosplit
b/snippets/easycrypt-mode/tactics/dosplit
new file mode 100644
index 0000000000..8c851d028b
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/dosplit
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: dosplit
+# key: dosplit
+# --
+do split.
+ + $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/ecall
b/snippets/easycrypt-mode/tactics/ecall
new file mode 100644
index 0000000000..81ec1a92b6
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/ecall
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: ecall
+# key: ecall
+# expand-env: ((yas-indent-line 'fixed))
+# --
+ecall ($1).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/ecall-wp
b/snippets/easycrypt-mode/tactics/ecall-wp
new file mode 100644
index 0000000000..15ed6ecc99
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/ecall-wp
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: ecall-wp
+# key: ecall-wp
+# expand-env: ((yas-indent-line 'fixed))
+# --
+ecall ($1); wp.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/elim-proof-term
b/snippets/easycrypt-mode/tactics/elim-proof-term
new file mode 100644
index 0000000000..2ebdff3ce1
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/elim-proof-term
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: elim-proof-term
+# key: elim-proof-term
+# expand-env: ((yas-indent-line 'fixed))
+# --
+elim /$1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/elim-var
b/snippets/easycrypt-mode/tactics/elim-var
new file mode 100644
index 0000000000..1b4884c36a
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/elim-var
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: elim-var
+# key: elim-var
+# expand-env: ((yas-indent-line 'fixed))
+# --
+elim: $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/exists
b/snippets/easycrypt-mode/tactics/exists
new file mode 100644
index 0000000000..d36e759420
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/exists
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: exists
+# key: exists
+# expand-env: ((yas-indent-line 'fixed))
+# --
+exists ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/exists-astreix1
b/snippets/easycrypt-mode/tactics/exists-astreix1
new file mode 100644
index 0000000000..26927b5590
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/exists-astreix1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: exists-astreix1
+# key: exists-astreix1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+exists* ($1){1}, ($2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/exists-astrix
b/snippets/easycrypt-mode/tactics/exists-astrix
new file mode 100644
index 0000000000..642074cc88
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/exists-astrix
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: exists-astrix
+# key: exists-astreix
+# expand-env: ((yas-indent-line 'fixed))
+# --
+exists* ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/first-last
b/snippets/easycrypt-mode/tactics/first-last
new file mode 100644
index 0000000000..247ad43c4c
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/first-last
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: first-last
+# key: first-last
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1; first last
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/first-n-last
b/snippets/easycrypt-mode/tactics/first-n-last
new file mode 100644
index 0000000000..ee8eb6e272
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/first-n-last
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: first-n-last
+# key:
+# --
+$1; first $2 last
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/firstn
b/snippets/easycrypt-mode/tactics/firstn
new file mode 100644
index 0000000000..309d68c61d
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/firstn
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: firstn
+# key: firstn
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1; first $2 $3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/fission
b/snippets/easycrypt-mode/tactics/fission
new file mode 100644
index 0000000000..d0950b1b8c
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/fission
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: fission
+# key: fission
+# expand-env: ((yas-indent-line 'fixed))
+# --
+fission $1!$2 @ $3, $4
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/fission1
b/snippets/easycrypt-mode/tactics/fission1
new file mode 100644
index 0000000000..c1da1102a6
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/fission1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: fission1
+# key: fission1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+fission{1} $1!$2 @ $3, $4
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/fission2
b/snippets/easycrypt-mode/tactics/fission2
new file mode 100644
index 0000000000..62a6c30ad0
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/fission2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: fission2
+# key: fission2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+fission{2} $1!$2 @ $3, $4
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/fusion
b/snippets/easycrypt-mode/tactics/fusion
new file mode 100644
index 0000000000..e5ccdf2af3
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/fusion
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: fusion
+# key: fusion
+# expand-env: ((yas-indent-line 'fixed))
+# --
+fusion $1!$2 @ $3, $4
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/fusion1
b/snippets/easycrypt-mode/tactics/fusion1
new file mode 100644
index 0000000000..9e31624f64
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/fusion1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: fusion1
+# key: fusion1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+fusion{1} $1!$2 @ $3, $4
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/fusion2
b/snippets/easycrypt-mode/tactics/fusion2
new file mode 100644
index 0000000000..d86c978961
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/fusion2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: fusion2
+# key: fusion2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+fusion{2} $1!$2 @ $3, $4
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/have-define
b/snippets/easycrypt-mode/tactics/have-define
new file mode 100644
index 0000000000..9b8de18c03
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/have-define
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: have-define
+# key: have-define
+# expand-env: ((yas-indent-line 'fixed))
+# --
+have := $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/have-introduce
b/snippets/easycrypt-mode/tactics/have-introduce
new file mode 100644
index 0000000000..690c887bbd
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/have-introduce
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: have-introduce
+# key: have-introduce
+# expand-env: ((yas-indent-line 'fixed))
+# --
+have $1: $2.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/have-write-left
b/snippets/easycrypt-mode/tactics/have-write-left
new file mode 100644
index 0000000000..162c18592d
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/have-write-left
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: have-write-left
+# key: have-write-left
+# expand-env: ((yas-indent-line 'fixed))
+# --
+have <-: $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/have-write-left-eq
b/snippets/easycrypt-mode/tactics/have-write-left-eq
new file mode 100644
index 0000000000..f4c952b2a4
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/have-write-left-eq
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: have-write-left-eq
+# key: have-write-left-eq
+# expand-env: ((yas-indent-line 'fixed))
+# --
+have <-: ($1) = ($2).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/have-write-right
b/snippets/easycrypt-mode/tactics/have-write-right
new file mode 100644
index 0000000000..7a70603c92
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/have-write-right
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: have-write-right
+# key: have-write-right
+# expand-env: ((yas-indent-line 'fixed))
+# --
+have ->: $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/have-write-right-eq
b/snippets/easycrypt-mode/tactics/have-write-right-eq
new file mode 100644
index 0000000000..872413ada7
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/have-write-right-eq
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: have-write-right-eq
+# key: have-wrtie-right-eq
+# expand-env: ((yas-indent-line 'fixed))
+# --
+have ->: ($1) = ($2).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/if
b/snippets/easycrypt-mode/tactics/if
new file mode 100644
index 0000000000..3aad147439
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/if
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: if
+# key: if
+# --
+if ($1) {
+
+}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/if1
b/snippets/easycrypt-mode/tactics/if1
new file mode 100644
index 0000000000..7b77179d35
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/if1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: if1
+# key: if1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+if{1}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/if2
b/snippets/easycrypt-mode/tactics/if2
new file mode 100644
index 0000000000..f7c66f3362
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/if2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: if2
+# key: if2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+if{2}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/implies
b/snippets/easycrypt-mode/tactics/implies
new file mode 100644
index 0000000000..c0b343df10
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/implies
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: implies
+# key: implies
+# --
+$1 => $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/implies-brackets
b/snippets/easycrypt-mode/tactics/implies-brackets
new file mode 100644
index 0000000000..490e1ed037
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/implies-brackets
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: implies-brackets
+# key: implies-brackets
+# --
+($1 => $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/inline
b/snippets/easycrypt-mode/tactics/inline
new file mode 100644
index 0000000000..e2937db504
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/inline
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: inline
+# key: inline
+# --
+inline {$1} ($2).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/inline1
b/snippets/easycrypt-mode/tactics/inline1
new file mode 100644
index 0000000000..e8c4c4f857
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/inline1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: inline1
+# key: inline1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+inline{1} ($1).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/inline2
b/snippets/easycrypt-mode/tactics/inline2
new file mode 100644
index 0000000000..99f118f955
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/inline2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: inline2
+# key: inline2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+inline{2} ($1).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/last
b/snippets/easycrypt-mode/tactics/last
new file mode 100644
index 0000000000..0c75255857
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/last
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: last
+# key: last
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1; last $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/last-first
b/snippets/easycrypt-mode/tactics/last-first
new file mode 100644
index 0000000000..3c034b5348
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/last-first
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: last-first
+# key: last-first
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1; last first
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/last-n-first
b/snippets/easycrypt-mode/tactics/last-n-first
new file mode 100644
index 0000000000..dae2795ed7
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/last-n-first
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: last-n-first
+# key: last-n-first
+# expand-env: ((yas-indent-line 'fixed))
+# --
+$1; last $2 first
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/lastn
b/snippets/easycrypt-mode/tactics/lastn
new file mode 100644
index 0000000000..23aaece6af
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/lastn
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: lastn
+# key: lastn
+# expand-env: ((yas-indent-line 'fixed))
+# --
+τ1; last $1 $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/move-1
b/snippets/easycrypt-mode/tactics/move-1
new file mode 100644
index 0000000000..fcf415fbcf
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/move-1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: move-1
+# key: move-1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+move => &1 $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/move-1m2
b/snippets/easycrypt-mode/tactics/move-1m2
new file mode 100644
index 0000000000..8d34502294
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/move-1m2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: move-1m2
+# key: move-1m2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+move => &1 &m &2 $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/move-2
b/snippets/easycrypt-mode/tactics/move-2
new file mode 100644
index 0000000000..22f0d47faf
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/move-2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: move-2
+# key: move-2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+move => &2 $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/move-from-assumption
b/snippets/easycrypt-mode/tactics/move-from-assumption
new file mode 100644
index 0000000000..bab2f09fd6
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/move-from-assumption
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: move-from-assumption
+# key: move-from-assumption
+# expand-env: ((yas-indent-line 'fixed))
+# --
+move : $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/move-hr
b/snippets/easycrypt-mode/tactics/move-hr
new file mode 100644
index 0000000000..0b0f944dcc
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/move-hr
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: move-hr
+# key: move-hr
+# expand-env: ((yas-indent-line 'fixed))
+# --
+move => &hr $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/move-lemma-args
b/snippets/easycrypt-mode/tactics/move-lemma-args
new file mode 100644
index 0000000000..6b8ab892a9
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/move-lemma-args
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: move-lemma-args
+# key: move-lemma-args
+# expand-env: ((yas-indent-line 'fixed))
+# --
+move: ($1 $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/move-to-assumption
b/snippets/easycrypt-mode/tactics/move-to-assumption
new file mode 100644
index 0000000000..ba2b63e1f8
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/move-to-assumption
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: move-to-assumption
+# key: move-to-assumptions
+# expand-env: ((yas-indent-line 'fixed))
+# --
+move => $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/pose
b/snippets/easycrypt-mode/tactics/pose
new file mode 100644
index 0000000000..fd4570fb17
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/pose
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: pose
+# key: pose
+# expand-env: ((yas-indent-line 'fixed))
+# --
+pose $1 := $2.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/proc-simplify
b/snippets/easycrypt-mode/tactics/proc-simplify
new file mode 100644
index 0000000000..71c3d83234
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/proc-simplify
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: proc-simplify
+# key: proc-simplify
+# expand-env: ((yas-indent-line 'fixed))
+# --
+proc => //=.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/proc-up-to-bad
b/snippets/easycrypt-mode/tactics/proc-up-to-bad
new file mode 100644
index 0000000000..18acb9068e
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/proc-up-to-bad
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: proc-up-to-bad
+# key: proc-up-to-bad
+# expand-env: ((yas-indent-line 'fixed))
+# --
+proc $1 ($2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/proc-up-to-bad2
b/snippets/easycrypt-mode/tactics/proc-up-to-bad2
new file mode 100644
index 0000000000..60406e8ac9
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/proc-up-to-bad2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: proc-up-to-bad2
+# key: proc-up-to-bad2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+proc $1 ($2) ($3)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rcondf1
b/snippets/easycrypt-mode/tactics/rcondf1
new file mode 100644
index 0000000000..5b85292f2c
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rcondf1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rcondf1
+# key: rcondf1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rcondf{1} $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rcondf2
b/snippets/easycrypt-mode/tactics/rcondf2
new file mode 100644
index 0000000000..9ad128fa94
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rcondf2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rcondf2
+# key: rcondf2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rcondf{2} $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rcondt-rl
b/snippets/easycrypt-mode/tactics/rcondt-rl
new file mode 100644
index 0000000000..c4a6c9246e
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rcondt-rl
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: rcondt-equiv
+# key: rcondt-prog
+# --
+rcondt {$1} $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rcondt1
b/snippets/easycrypt-mode/tactics/rcondt1
new file mode 100644
index 0000000000..a013f4d1cd
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rcondt1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rcondt1
+# key: rcondt1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rcondt{1} $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rcondt2
b/snippets/easycrypt-mode/tactics/rcondt2
new file mode 100644
index 0000000000..5364a0ada9
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rcondt2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rcondt2
+# key: rcondt2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rcondt{2} $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/repeat-from-to
b/snippets/easycrypt-mode/tactics/repeat-from-to
new file mode 100644
index 0000000000..ef8bd361f5
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/repeat-from-to
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: repeat-from-to
+# key: repeat-from-to
+# expand-env: ((yas-indent-line 'fixed))
+# --
+[$1..$2]!$3
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rewrite
b/snippets/easycrypt-mode/tactics/rewrite
new file mode 100644
index 0000000000..d174f8c723
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rewrite
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rewrite
+# key: rewrite
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rewrite $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rewrite-crush
b/snippets/easycrypt-mode/tactics/rewrite-crush
new file mode 100644
index 0000000000..b0a7f9e819
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rewrite-crush
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rewrite-crush
+# key: rewrite-crush
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rewrite $1 => />.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rewrite-expand-list
b/snippets/easycrypt-mode/tactics/rewrite-expand-list
new file mode 100644
index 0000000000..88897f1e3a
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rewrite-expand-list
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rewrite-expand-list
+# key: rewrite-expand-list
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rewrite $1 !/mkseq -iotaredE => />.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rewrite-fun-backwards
b/snippets/easycrypt-mode/tactics/rewrite-fun-backwards
new file mode 100644
index 0000000000..6f3ffb1e81
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rewrite-fun-backwards
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rewrite-lemma-backwards-args
+# key: rewrite-lemma-backwards-args
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rewrite -($1 $2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rewrite-in
b/snippets/easycrypt-mode/tactics/rewrite-in
new file mode 100644
index 0000000000..66f9067598
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rewrite-in
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rewrite-in
+# key: rewrite-in
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rewrite $1 in $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rewrite-lemma-forwards-args
b/snippets/easycrypt-mode/tactics/rewrite-lemma-forwards-args
new file mode 100644
index 0000000000..09c6e653dd
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rewrite-lemma-forwards-args
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rewrite-lemma-forwards-args
+# key: rewrite-lemma-forward-args
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rewrite ($1 $2).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rewrite-proof-term-in
b/snippets/easycrypt-mode/tactics/rewrite-proof-term-in
new file mode 100644
index 0000000000..b45f847fe7
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rewrite-proof-term-in
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rewrite-proof-term-in
+# key: rewrite-proof-term-in
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rewrite /$1 in $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rnd-f
b/snippets/easycrypt-mode/tactics/rnd-f
new file mode 100644
index 0000000000..b5d8be11b1
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rnd-f
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rnd-f
+# key: rnd-f
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rnd ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rnd-fg
b/snippets/easycrypt-mode/tactics/rnd-fg
new file mode 100644
index 0000000000..e248f2e27b
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rnd-fg
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rnd-fg
+# key: rnd-fg
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rnd ($1) ($2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rnd1
b/snippets/easycrypt-mode/tactics/rnd1
new file mode 100644
index 0000000000..fe76423cfd
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rnd1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rnd1
+# key: rnd1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rnd{1}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/rnd2
b/snippets/easycrypt-mode/tactics/rnd2
new file mode 100644
index 0000000000..2ba7defe75
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/rnd2
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: rnd2
+# key: rnd2
+# --
+rnd{2}
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/seq
b/snippets/easycrypt-mode/tactics/seq
new file mode 100644
index 0000000000..a4168b5276
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/seq
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: seq
+# key: seq
+# expand-env: ((yas-indent-line 'fixed))
+# --
+seq $1 $2 : ($3)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/sim
b/snippets/easycrypt-mode/tactics/sim
new file mode 100644
index 0000000000..6302423203
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/sim
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: sim
+# key: sim
+# expand-env: ((yas-indent-line 'fixed))
+# --
+sim ($1) / ($2) : ($3)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/smt
b/snippets/easycrypt-mode/tactics/smt
new file mode 100644
index 0000000000..05af5c5f8e
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/smt
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: smt
+# key: smt
+# expand-env: ((yas-indent-line 'fixed))
+# --
+smt().
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/splitwhile
b/snippets/easycrypt-mode/tactics/splitwhile
new file mode 100644
index 0000000000..48aad2d7ba
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/splitwhile
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: splitwhile
+# key: splitwhile
+# expand-env: ((yas-indent-line 'fixed))
+# --
+splitwhile $1 : ($2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/splitwhile1
b/snippets/easycrypt-mode/tactics/splitwhile1
new file mode 100644
index 0000000000..1259571744
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/splitwhile1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: splitwhile1
+# key: splitwhile1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+splitwhile{1} $1 : ($2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/splitwhile2
b/snippets/easycrypt-mode/tactics/splitwhile2
new file mode 100644
index 0000000000..67d2d8bbac
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/splitwhile2
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: splitwhile2
+# key: splitwhile2
+# expand-env: ((yas-indent-line 'fixed))
+# --
+splitwhile{2} $1 : ($2)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/transitivity
b/snippets/easycrypt-mode/tactics/transitivity
new file mode 100644
index 0000000000..a947dd17f0
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/transitivity
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: transitivity
+# key: transitivity
+# expand-env: ((yas-indent-line 'fixed))
+# --
+transitivity $1
+ ($2 ==> $3)
+ ($4 ==> $5).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/transitivity-code
b/snippets/easycrypt-mode/tactics/transitivity-code
new file mode 100644
index 0000000000..8ef804d8cd
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/transitivity-code
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: transitivity-code
+# key: transitivity-code
+# expand-env: ((yas-indent-line 'fixed))
+# --
+transitivity{$1} {$2;}
+ ($2 ==> $3)
+ ($4 ==> $5).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/unroll-equiv
b/snippets/easycrypt-mode/tactics/unroll-equiv
new file mode 100644
index 0000000000..3c231fe6f2
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/unroll-equiv
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: unroll-equiv
+# key: unroll-prog
+# expand-env: ((yas-indent-line 'fixed))
+# --
+unroll {$1} $2
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/unroll-while
b/snippets/easycrypt-mode/tactics/unroll-while
new file mode 100644
index 0000000000..7df6ce4d32
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/unroll-while
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: unroll-while
+# key: unroll
+# expand-env: ((yas-indent-line 'fixed))
+# --
+unroll for{$1} ^while
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/while
b/snippets/easycrypt-mode/tactics/while
new file mode 100644
index 0000000000..51039a6d36
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/while
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: while
+# key: while
+# expand-env: ((yas-indent-line 'fixed))
+# --
+while(
+
+).
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/while-true
b/snippets/easycrypt-mode/tactics/while-true
new file mode 100644
index 0000000000..c3607d67dd
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/while-true
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: while-true
+# key: while-true
+# expand-env: ((yas-indent-line 'fixed))
+# --
+while true $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/while1
b/snippets/easycrypt-mode/tactics/while1
new file mode 100644
index 0000000000..63e7af8364
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/while1
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: while1
+# key: while1
+# expand-env: ((yas-indent-line 'fixed))
+# --
+while{1} ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/tactics/while2
b/snippets/easycrypt-mode/tactics/while2
new file mode 100644
index 0000000000..48c48a16f5
--- /dev/null
+++ b/snippets/easycrypt-mode/tactics/while2
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: tactics
+# name: while2
+# key:
+# --
+while{2} ($1)
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/abstract-theory
b/snippets/easycrypt-mode/theories/abstract-theory
new file mode 100644
index 0000000000..c08957488b
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/abstract-theory
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: abstract-theory
+# key: abstract-theory
+# expand-env: ((yas-indent-line 'fixed))
+# --
+abstract theory $1.
+
+
+end $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/clone-as
b/snippets/easycrypt-mode/theories/clone-as
new file mode 100644
index 0000000000..15d2088057
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/clone-as
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: clone-as
+# key: clone-as
+# expand-env: ((yas-indent-line 'fixed))
+# --
+clone $1 as $2.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/clone-as-with
b/snippets/easycrypt-mode/theories/clone-as-with
new file mode 100644
index 0000000000..d8df96e78e
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/clone-as-with
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: clone-as-with
+# key: clone-as-with
+# expand-env: ((yas-indent-line 'fixed))
+# --
+clone $1 as $2 with
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/clone-import
b/snippets/easycrypt-mode/theories/clone-import
new file mode 100644
index 0000000000..996348d5c1
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/clone-import
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: clone-import
+# key: clone-import
+# expand-env: ((yas-indent-line 'fixed))
+# --
+clone import $1 as $2 with
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/clone-include
b/snippets/easycrypt-mode/theories/clone-include
new file mode 100644
index 0000000000..ff08571de8
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/clone-include
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: clone-include
+# key: clone-include
+# expand-env: ((yas-indent-line 'fixed))
+# --
+clone include $1
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/clone-no-with
b/snippets/easycrypt-mode/theories/clone-no-with
new file mode 100644
index 0000000000..12f9c5976c
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/clone-no-with
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# name: clone-no-with
+# key: clone-no-with
+# --
+clone $1 as $2.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/rename-as
b/snippets/easycrypt-mode/theories/rename-as
new file mode 100644
index 0000000000..42b7848d90
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/rename-as
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: rename-as
+# key: rename-as
+# expand-env: ((yas-indent-line 'fixed))
+# --
+rename "$1" as "$2"
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/section
b/snippets/easycrypt-mode/theories/section
new file mode 100644
index 0000000000..5589fc6fb7
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/section
@@ -0,0 +1,10 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: section
+# key: section
+# expand-env: ((yas-indent-line 'fixed))
+# --
+section.
+
+end section.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/theory
b/snippets/easycrypt-mode/theories/theory
new file mode 100644
index 0000000000..4848879d14
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/theory
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: theory
+# key: theory
+# expand-env: ((yas-indent-line 'fixed))
+# --
+theory $1.
+
+
+end $1.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/type
b/snippets/easycrypt-mode/theories/type
new file mode 100644
index 0000000000..ce0a66e802
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/type
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: type
+# key: type
+# expand-env: ((yas-indent-line 'fixed))
+# --
+type $1 = $2.
\ No newline at end of file
diff --git a/snippets/easycrypt-mode/theories/with
b/snippets/easycrypt-mode/theories/with
new file mode 100644
index 0000000000..81758d2a02
--- /dev/null
+++ b/snippets/easycrypt-mode/theories/with
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# contributor: João Diogo Duarte
+# group: theories
+# name: with
+# key: with
+# expand-env: ((yas-indent-line 'fixed))
+# --
+with $1 => $2
\ No newline at end of file
