~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/refman/Extraction.tex

• browse files at revision 6
• compare with another revision
• download diff
• download tarball
• view history from revision 6

Show diffs side-by-side

added

removed

doc/refman/Extraction.tex

334

334

{\tt nat} into Ocaml's {\tt int} (see caveat above):

335

335

\begin{coq_example}

336

336

Extract Inductive nat => int [ "0" "succ" ]

337

 

 "(fun fO fS n => if n=0 then fO () else fS (n-1))".

 

337

 "(fun fO fS n -> if n=0 then fO () else fS (n-1))".

338

338

\end{coq_example}

339

339

 

340

340

\asubsection{Avoiding conflicts with existing filenames}

543

543

 After compilation those two examples run nonetheless,

544

544

 thanks to the correction of the extraction~\cite{Let02}. 

545

545

 

546

 

% $Id: Extraction.tex 13153 2010-06-15 16:09:43Z letouzey $ 

 

546

% $Id: Extraction.tex 14575 2011-10-18 15:49:01Z letouzey $ 

547

547

 

548

548

%%% Local Variables: 

549

549

%%% mode: latex

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1