Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (8 years ago)
Author:
sacerdot
Message:
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1351 r1451  
    120120    ]
    121121].
     122
     123let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
     124match l with
     125[ nil ⇒ None ?
     126| cons h t ⇒
     127   match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
     128
     129definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
     130 λA,found,l. position_of_aux A found l 0.
Note: See TracChangeset for help on using the changeset viewer.