From b72c81f8090c1326fe819ea4c0a2714c0944b8e8 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 29 Jan 2016 14:59:42 +0100
Subject: Import EasyCrypt PG mode

---
 easycrypt/easycrypt-keywords.el | 168 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 168 insertions(+)
 create mode 100644 easycrypt/easycrypt-keywords.el

(limited to 'easycrypt/easycrypt-keywords.el')

diff --git a/easycrypt/easycrypt-keywords.el b/easycrypt/easycrypt-keywords.el
new file mode 100644
index 00000000..53b695ff
--- /dev/null
+++ b/easycrypt/easycrypt-keywords.el
@@ -0,0 +1,168 @@
+; Generated on Thu Dec 17 16:14:05 2015
+
+(defvar easycrypt-bytac-keywords '(
+  "exact"
+  "assumption"
+  "smt"
+  "by"
+  "reflexivity"
+  "done"
+))
+
+(defvar easycrypt-dangerous-keywords '(
+  "admit"
+  "admitted"
+))
+
+(defvar easycrypt-global-keywords '(
+  "axiom"
+  "axiomatized"
+  "lemma"
+  "realize"
+  "proof"
+  "qed"
+  "abort"
+  "goal"
+  "end"
+  "import"
+  "export"
+  "include"
+  "local"
+  "declare"
+  "hint"
+  "nosmt"
+  "module"
+  "of"
+  "const"
+  "op"
+  "pred"
+  "notation"
+  "abbrev"
+  "require"
+  "theory"
+  "abstract"
+  "section"
+  "type"
+  "class"
+  "instance"
+  "print"
+  "search"
+  "as"
+  "Pr"
+  "clone"
+  "with"
+  "rename"
+  "prover"
+  "timeout"
+  "why3"
+  "dump"
+  "remove"
+  "Top"
+  "Self"
+))
+
+(defvar easycrypt-internal-keywords '(
+  "time"
+  "undo"
+  "debug"
+  "pragma"
+))
+
+(defvar easycrypt-prog-keywords '(
+  "forall"
+  "exists"
+  "fun"
+  "glob"
+  "let"
+  "in"
+  "var"
+  "proc"
+  "if"
+  "then"
+  "else"
+  "elif"
+  "while"
+  "assert"
+  "return"
+  "res"
+  "equiv"
+  "hoare"
+  "phoare"
+  "islossless"
+))
+
+(defvar easycrypt-tactic-keywords '(
+  "beta"
+  "iota"
+  "zeta"
+  "eta"
+  "logic"
+  "delta"
+  "simplify"
+  "congr"
+  "change"
+  "split"
+  "left"
+  "right"
+  "case"
+  "pose"
+  "cut"
+  "have"
+  "suff"
+  "elim"
+  "clear"
+  "apply"
+  "rewrite"
+  "rwnormal"
+  "subst"
+  "progress"
+  "trivial"
+  "auto"
+  "idtac"
+  "move"
+  "modpath"
+  "field"
+  "fieldeq"
+  "ring"
+  "ringeq"
+  "algebra"
+  "transitivity"
+  "symmetry"
+  "seq"
+  "wp"
+  "sp"
+  "sim"
+  "skip"
+  "call"
+  "rcondt"
+  "rcondf"
+  "swap"
+  "cfold"
+  "rnd"
+  "pr_bounded"
+  "bypr"
+  "byphoare"
+  "byequiv"
+  "fel"
+  "conseq"
+  "exfalso"
+  "inline"
+  "alias"
+  "fission"
+  "fusion"
+  "unroll"
+  "splitwhile"
+  "kill"
+  "eager"
+))
+
+(defvar easycrypt-tactical-keywords '(
+  "try"
+  "first"
+  "last"
+  "do"
+  "strict"
+  "expect"
+))
+
+(provide 'easycrypt-keywords)
-- 
cgit v1.2.3