Dafny: added iterators; for now, only parsing and resolving (and printing and refining), no compilation or verification

1 files changed, 5 insertions, 3 deletions

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 81b04694..88f9c2a2 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -5,15 +5,17 @@
 \usepackage{listings}

 

 \lstdefinelanguage{dafny}{

-  morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,map,%

+  morekeywords={class,datatype,codatatype,type,iterator,

+      bool,nat,int,object,set,multiset,seq,array,array2,array3,map,

       function,predicate,copredicate,

       ghost,var,static,refines,

-      method,constructor,returns,module,import,default,opened,as,in,

+      method,constructor,returns,yields,module,import,default,opened,as,in,

       requires,modifies,ensures,reads,decreases,free,

       % expressions

       match,case,false,true,null,old,fresh,choose,this,

       % statements

-      assert,assume,print,new,if,then,else,while,invariant,break,label,return,parallel,where

+      assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,

+      parallel,where

       },

   literate=%

     {:}{$\colon$}1