Mercurial > cpdt > repo

comparison src/DataStruct.v @ 204:cbf2f74a5130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parts I want to keep compile with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 10:52:43 -0500
parents 464db50b210a
children f05514cc6c0d
comparison
equal deleted inserted replaced
203:71ade09024ac 204:cbf2f74a5130
697 Fixpoint cfoldCond (n : nat) 697 Fixpoint cfoldCond (n : nat)
698 : (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t := 698 : (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t :=
699 match n return (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t with 699 match n return (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t with
700 | O => fun _ _ => default 700 | O => fun _ _ => default
701 | S n' => fun tests bodies => 701 | S n' => fun tests bodies =>
702 match tests None with 702 match tests None return _ with
703 | BConst true => bodies None 703 | BConst true => bodies None
704 | BConst false => cfoldCond n' 704 | BConst false => cfoldCond n'
705 (fun idx => tests (Some idx)) 705 (fun idx => tests (Some idx))
706 (fun idx => bodies (Some idx)) 706 (fun idx => bodies (Some idx))
707 | _ => 707 | _ =>
741 match e in exp' t return exp' t with 741 match e in exp' t return exp' t with
742 | NConst n => NConst n 742 | NConst n => NConst n
743 | Plus e1 e2 => 743 | Plus e1 e2 =>
744 let e1' := cfold e1 in 744 let e1' := cfold e1 in
745 let e2' := cfold e2 in 745 let e2' := cfold e2 in
746 match e1', e2' with 746 match e1', e2' return _ with
747 | NConst n1, NConst n2 => NConst (n1 + n2) 747 | NConst n1, NConst n2 => NConst (n1 + n2)
748 | _, _ => Plus e1' e2' 748 | _, _ => Plus e1' e2'
749 end 749 end
750 | Eq e1 e2 => 750 | Eq e1 e2 =>
751 let e1' := cfold e1 in 751 let e1' := cfold e1 in
752 let e2' := cfold e2 in 752 let e2' := cfold e2 in
753 match e1', e2' with 753 match e1', e2' return _ with
754 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false) 754 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
755 | _, _ => Eq e1' e2' 755 | _, _ => Eq e1' e2'
756 end 756 end
757 757
758 | BConst b => BConst b 758 | BConst b => BConst b