From c8472e7d649c8be8092a4607366a177b7e7307ef Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 25 Sep 2012 15:06:54 -0700 Subject: Dafny: added iterators; for now, only parsing and resolving (and printing and refining), no compilation or verification --- Util/latex/dafny.sty | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'Util/latex') 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 -- cgit v1.2.3