Changeset 1601 for src/joint/BEValues.ma


Ignore:
Timestamp:
Dec 13, 2011, 2:49:52 PM (9 years ago)
Author:
sacerdot
Message:

Files ported to new version of the standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEValues.ma

    r1516 r1601  
    33
    44include "common/Pointers.ma".
    5 include "utilities/sigma.ma".
    65
    76record part (r: region): Type[0] ≝
     
    121120  do p ← pointer_of_bevals [v1;v2] ;
    122121  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
    123   [ Code ⇒ λE.OK ? (inject … p ?)
     122  [ Code ⇒ λE.OK ? (mk_Sig … p ?)
    124123  | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
    125124// qed.
Note: See TracChangeset for help on using the changeset viewer.