Mercurial > cpdt > repo

comparison src/Subset.v @ 469:b36876d4611e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Batch of changes based on proofreader feedback
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Sep 2012 16:35:35 -0400
parents 822442bf6d7f
children 51a8472aca68
comparison
equal deleted inserted replaced
468:62475ab7570b 469:b36876d4611e
517 End In_dec. 517 End In_dec.
518 518
519 Eval compute in In_dec eq_nat_dec 2 (1 :: 2 :: nil). 519 Eval compute in In_dec eq_nat_dec 2 (1 :: 2 :: nil).
520 (** %\vspace{-.15in}% [[ 520 (** %\vspace{-.15in}% [[
521 = Yes 521 = Yes
522 : {In 2 (1 :: 2 :: nil)} + {~ In 2 (1 :: 2 :: nil)} 522 : {In 2 (1 :: 2 :: nil)} + { ~ In 2 (1 :: 2 :: nil)}
523 ]] 523 ]]
524 *) 524 *)
525 525
526 Eval compute in In_dec eq_nat_dec 3 (1 :: 2 :: nil). 526 Eval compute in In_dec eq_nat_dec 3 (1 :: 2 :: nil).
527 (** %\vspace{-.15in}% [[ 527 (** %\vspace{-.15in}% [[
528 = No 528 = No
529 : {In 3 (1 :: 2 :: nil)} + {~ In 3 (1 :: 2 :: nil)} 529 : {In 3 (1 :: 2 :: nil)} + { ~ In 3 (1 :: 2 :: nil)}
530 ]] 530 ]]
531 531
532 [In_dec] has a reasonable extraction to OCaml. *) 532 The [In_dec] function has a reasonable extraction to OCaml. *)
533 533
534 Extraction In_dec. 534 Extraction In_dec.
535 (* end thide *) 535 (* end thide *)
536 536
537 (** %\begin{verbatim} 537 (** %\begin{verbatim}