Changeset 647
 Timestamp:
 Mar 7, 2011, 7:00:01 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.1/Presentations/WP3brian.tex
r637 r647 10 10 \lstdefinelanguage{coq} 11 11 {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record}, 12 morekeywords={[2]if,then,else },12 morekeywords={[2]if,then,else,forall,Prop}, 13 13 } 14 14 15 15 \lstdefinelanguage{matita} 16 {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with, Type,and,on},17 morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct },16 {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,and,on,return}, 17 morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct,Prop,Type}, 18 18 mathescape=true, 19 19 } … … 82 82 \colorbox{lightgreen}{New code.} 83 83 \begin{itemize} 84 \item Prove nequivalent to the inductive semantics84 \item Proved equivalent to the inductive semantics 85 85 \end{itemize} 86 86 \end{frame} … … 323 323 \begin{itemize} 324 324 \item[$\triangleright$] proof terms get in the way later on 325 \item[$\triangleright$] providing separate theorems easier 325 326 \end{itemize} 326 \item Full executions trick er  final result requires ability to327 \item Full executions trickier  final result requires ability to 327 328 commit to (non)termination 328 329 \begin{itemize}
Note: See TracChangeset
for help on using the changeset viewer.