package fstar
-
fstar.lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val uu___is_LocBuffer : loc_aux -> Prims.boolval __proj__LocBuffer__item__b : loc_aux -> Prims.unit FStar_Buffer.buffertype ('l, 'r, 'n) loc_aux_in_addr = Obj.ttype ('r, 'n) aloc = loc_auxtype ('a, 's, 'b) loc_aux_includes_buffer = Obj.ttype ('s1, 's2) loc_aux_includes = Obj.ttype ('l, 't, 'p) loc_aux_disjoint_buffer = Obj.ttype ('l1, 'l2) loc_aux_disjoint = Obj.ttype ('l, 'h1, 'h2) loc_aux_preserved = Obj.ttype loc = Prims.unittype ('s1, 's2) loc_includes = Prims.unittype ('s1, 's2) loc_disjoint = Prims.unittype ('s, 'h1, 'h2) modifies = Prims.unittype ('h, 'ra) does_not_contain_addr = Prims.unittype ('uuuuu, 'uuuuu1) cloc_aloc = (Prims.unit, Prims.unit) aloc