Mercurial > cpdt > repo
comparison src/MoreDep.v @ 437:8077352044b2
A pass over all formatting, after big pile of coqdoc changes
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 27 Jul 2012 16:47:28 -0400 |
| parents | 5f25705a10ea |
| children | 97c60ffdb998 |
comparison
equal
deleted
inserted
replaced
| 436:5d5e44f905c7 | 437:8077352044b2 |
|---|---|
| 231 | 231 |
| 232 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) | 232 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) |
| 233 | Fst _ _ e' => fst (expDenote e') | 233 | Fst _ _ e' => fst (expDenote e') |
| 234 | Snd _ _ e' => snd (expDenote e') | 234 | Snd _ _ e' => snd (expDenote e') |
| 235 end. | 235 end. |
| 236 | |
| 237 (* begin hide *) | |
| 238 (* begin thide *) | |
| 239 Definition sumboool := sumbool. | |
| 240 (* end thide *) | |
| 241 (* end hide *) | |
| 236 | 242 |
| 237 (** Despite the fancy type, the function definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type. Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns. | 243 (** Despite the fancy type, the function definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type. Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns. |
| 238 | 244 |
| 239 We can implement our old favorite, a constant folding function, and prove it correct. It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error. | 245 We can implement our old favorite, a constant folding function, and prove it correct. It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error. |
| 240 | 246 |
| 525 Definition rpresent n (t : rtree n) : Prop := | 531 Definition rpresent n (t : rtree n) : Prop := |
| 526 match t with | 532 match t with |
| 527 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b | 533 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b |
| 528 end. | 534 end. |
| 529 End present. | 535 End present. |
| 530 | |
| 531 (* begin hide *) | |
| 532 Definition sigT' := sigT. | |
| 533 (* end hide *) | |
| 534 | 536 |
| 535 (** Insertion relies on two balancing operations. It will be useful to give types to these operations using a relative of the subset types from last chapter. While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently typed value. The %\index{Gallina terms!sigT}%[sigT] type fills this role. *) | 537 (** Insertion relies on two balancing operations. It will be useful to give types to these operations using a relative of the subset types from last chapter. While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently typed value. The %\index{Gallina terms!sigT}%[sigT] type fills this role. *) |
| 536 | 538 |
| 537 Locate "{ _ : _ & _ }". | 539 Locate "{ _ : _ & _ }". |
| 538 (** [[ | 540 (** [[ |