Changeset 780 for src/utilities


Ignore:
Timestamp:
Apr 28, 2011, 10:55:49 AM (10 years ago)
Author:
campbell
Message:

Properly update set of registers that are used for pointers in Cminor to
RTLabs phase.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r766 r780  
    66| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
    77].
     8
     9let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
     10match l with
     11[ nil ⇒ false
     12| cons h t ⇒ orb (p h) (exists A p t)
     13].
Note: See TracChangeset for help on using the changeset viewer.