Ignore:
Timestamp:
Mar 4, 2011, 6:20:26 PM (9 years ago)
Author:
campbell
Message:

A few definitions that will be useful for some preliminary rtlabs semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Errors.ma

    r487 r636  
    1616include "basics/types.ma".
    1717include "basics/logic.ma".
     18include "basics/list.ma".
    1819
    1920(* * Error reporting and the error monad. *)
     
    107108
    108109(** This is the familiar monadic map iterator. *)
    109 
    110 Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
     110*)
     111
     112let rec mmap (A, B: Type[0]) (f: A → res B) (l: list A) on l : res (list B) ≝
    111113  match l with
    112   | nil => OK nil
    113   | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl')
    114   end.
    115 
    116 Remark mmap_inversion:
    117   forall (A B: Type) (f: A -> res B) (l: list A) (l': list B),
    118   mmap f l = OK l' ->
     114  [ nil ⇒ OK ? []
     115  | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
     116  ].
     117
     118(*
     119lemma mmap_inversion:
     120  ∀A, B: Type[0]. ∀f: A -> res B. ∀l: list A. ∀l': list B.
     121  mmap A B f l = OK ? l' →
    119122  list_forall2 (fun x y => f x = OK y) l l'.
    120123Proof.
Note: See TracChangeset for help on using the changeset viewer.