Changeset 816 for src/utilities/lists.ma


Ignore:
Timestamp:
May 19, 2011, 3:06:42 PM (10 years ago)
Author:
campbell
Message:

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r780 r816  
    77].
    88
     9let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
     10match l with
     11[ nil ⇒ False
     12| cons h t ⇒ P h ∧ All A P t
     13].
     14
    915let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
    1016match l with
Note: See TracChangeset for help on using the changeset viewer.