Mercurial > cpdt > repo

comparison src/MoreDep.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents b441010125d4
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
150 : forall n : nat, ilist n -> match n with 150 : forall n : nat, ilist n -> match n with
151 | 0 => unit 151 | 0 => unit
152 | S _ => A 152 | S _ => A
153 end 153 end
154 154
155 ]] *) 155 ]]
156 *)
156 157
157 Definition hd n (ls : ilist (S n)) : A := hd' ls. 158 Definition hd n (ls : ilist (S n)) : A := hd' ls.
158 (* end thide *) 159 (* end thide *)
159 160
160 (** We annotate our main [match] with a type that is itself a [match]. We write that the function [hd'] returns [unit] when the list is empty and returns the carried type [A] in all other cases. In the definition of [hd], we just call [hd']. Because the index of [ls] is known to be nonzero, the type checker reduces the [match] in the type of [hd'] to [A]. *) 161 (** We annotate our main [match] with a type that is itself a [match]. We write that the function [hd'] returns [unit] when the list is empty and returns the carried type [A] in all other cases. In the definition of [hd], we just call [hd']. Because the index of [ls] is known to be nonzero, the type checker reduces the [match] in the type of [hd'] to [A]. *)
418 Check min_dec. 419 Check min_dec.
419 (** %\vspace{-.15in}% [[ 420 (** %\vspace{-.15in}% [[
420 min_dec 421 min_dec
421 : forall n m : nat, {min n m = n} + {min n m = m} 422 : forall n m : nat, {min n m = n} + {min n m = m}
422 423
423 ]] *) 424 ]]
425 *)
424 426
425 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n. 427 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
426 induction t; crush; 428 induction t; crush;
427 match goal with 429 match goal with
428 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y) 430 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
510 512
511 Locate "{ _ : _ & _ }". 513 Locate "{ _ : _ & _ }".
512 (** [[ 514 (** [[
513 Notation Scope 515 Notation Scope
514 "{ x : A & P }" := sigT (fun x : A => P) 516 "{ x : A & P }" := sigT (fun x : A => P)
515 ]] *) 517 ]]
518 *)
516 519
517 Print sigT. 520 Print sigT.
518 (** [[ 521 (** [[
519 Inductive sigT (A : Type) (P : A -> Type) : Type := 522 Inductive sigT (A : Type) (P : A -> Type) : Type :=
520 existT : forall x : A, P x -> sigT P 523 existT : forall x : A, P x -> sigT P
521 ]] *) 524 ]]
525 *)
522 526
523 (** It will be helpful to define a concise notation for the constructor of [sigT]. *) 527 (** It will be helpful to define a concise notation for the constructor of [sigT]. *)
524 528
525 Notation "{< x >}" := (existT _ _ x). 529 Notation "{< x >}" := (existT _ _ x).
526 530