Changeset 1874 for src/joint


Ignore:
Timestamp:
Apr 4, 2012, 6:48:25 PM (8 years ago)
Author:
campbell
Message:

First cut at using back-end memory model throughout.
Note the correction to BEValues.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEValues.ma

    r1601 r1874  
    66record part (r: region): Type[0] ≝
    77 { part_no:> nat
    8  ; part_no_ok: part_no size_pointer r
     8 ; part_no_ok: part_no < size_pointer r
    99 }.
    1010
Note: See TracChangeset for help on using the changeset viewer.