diff options
| author |  Rustan Leino <unknown> | 2013-08-02 21:44:37 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-02 21:44:37 -0700 |
| commit | 8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 (patch) | |
| tree | f412217ac7bb4e348669f9b34d121349c187e294 /Util | |
| parent | 0487bbe1d95c08a458e496240547127f03a7be3b (diff) | |
Introduced keywords "lemma" (like a "ghost method", but not allowed to have a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
Diffstat (limited to 'Util')
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 2 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/dafny.vim | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index b043150c..c59de6ed 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -32,7 +32,7 @@ `(,(dafny-regexp-opt '(
"class" "datatype" "codatatype" "type" "iterator"
"function" "predicate" "copredicate"
- "ghost" "var" "method" "constructor" "comethod"
+ "ghost" "var" "method" "lemma" "constructor" "comethod" "colemma"
"abstract" "module" "import" "default" "as" "opened" "static" "refines"
"returns" "yields" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 6982f032..d8d4ad96 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -9,7 +9,7 @@ bool,nat,int,object,set,multiset,seq,array,array2,array3,map,
function,predicate,copredicate,
ghost,var,static,refines,
- method,constructor,comethod,
+ method,lemma,constructor,comethod,colemma,
returns,yields,abstract,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index 31f27c51..414b5fdc 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -6,7 +6,7 @@ syntax clear syntax case match syntax keyword dafnyFunction function predicate copredicate -syntax keyword method constructor comethod +syntax keyword method lemma constructor comethod colemma syntax keyword dafnyTypeDef class datatype codatatype type iterator syntax keyword abstract module import opened as default syntax keyword dafnyConditional if then else match case |