Mercurial > cpdt > repo

comparison src/Extensional.v @ 225:19902d0b6622

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix Extensional type annotations
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 13:13:34 -0500
parents 4b73ea13574d
children 0400fa005d5a
comparison
equal deleted inserted replaced
224:4b73ea13574d 225:19902d0b6622
525 525
526 Fixpoint matchesDenote (tss : list (list type)) 526 Fixpoint matchesDenote (tss : list (list type))
527 : (forall ts, member ts tss -> option (hlist typeDenote ts)) 527 : (forall ts, member ts tss -> option (hlist typeDenote ts))
528 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2) 528 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
529 -> typeDenote t2 := 529 -> typeDenote t2 :=
530 match tss with 530 match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
531 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
532 -> _ with
531 | nil => fun _ _ => 533 | nil => fun _ _ =>
532 default 534 default
533 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') 535 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss')
534 -> option (hlist typeDenote ts')) 536 -> option (hlist typeDenote ts'))
535 (bodies : forall ts', member ts' (ts :: tss') 537 (bodies : forall ts', member ts' (ts :: tss')
797 Fixpoint elaborateMatches var t1 t2 799 Fixpoint elaborateMatches var t1 t2
798 (tss : list (list type)) 800 (tss : list (list type))
799 : (forall ts, member ts tss -> pat t1 ts) 801 : (forall ts, member ts tss -> pat t1 ts)
800 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2) 802 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
801 -> choice_tree var t1 (option (Elab.exp var t2)) := 803 -> choice_tree var t1 (option (Elab.exp var t2)) :=
802 match tss with 804 match tss return (forall ts, member ts tss -> pat t1 ts)
805 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
806 -> _ with
803 | nil => fun _ _ => 807 | nil => fun _ _ =>
804 everywhere (fun _ => None) 808 everywhere (fun _ => None)
805 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts') 809 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
806 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) => 810 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
807 merge (@mergeOpt _) 811 merge (@mergeOpt _)