diff options
| author |  Pierre-Yves Strub <pierre-yves@strub.nu> | 2016-01-29 14:59:42 +0100 |
|---|---|---|
| committer | Pierre-Yves Strub <pierre-yves@strub.nu> | 2016-01-29 14:59:42 +0100 |
| commit | b72c81f8090c1326fe819ea4c0a2714c0944b8e8 (patch) | |
| tree | ef871c03f9cfa071ba70ba6c344fd05fa8676bef /easycrypt/easycrypt-keywords.el | |
| parent | 626013259652e208ce99c84463e05ce22e62484a (diff) | |
Import EasyCrypt PG mode
Diffstat (limited to 'easycrypt/easycrypt-keywords.el')
| -rw-r--r-- | easycrypt/easycrypt-keywords.el | 168 |
1 files changed, 168 insertions, 0 deletions
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) |