Changeset 1551


Ignore:
Timestamp:
Nov 24, 2011, 11:52:52 AM (8 years ago)
Author:
campbell
Message:

Functions to translate between back-end and front-end values.

Location:
src
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1516 r1551  
    129129definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
    130130 λA,found,l. position_of_aux A found l 0.
     131 
     132
     133let rec make_list (A:Type[0]) (a:A) (n:nat) on n : list A ≝
     134match n with
     135[ O ⇒ [ ]
     136| S m ⇒ a::(make_list A a m)
     137].
  • src/utilities/option.ma

    r1316 r1551  
    1616] qed.
    1717
     18definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝
     19λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
     20
    1821lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
    1922  (∀v. x = Some ? v → Q (P v)) →
Note: See TracChangeset for help on using the changeset viewer.