source: extracted/frontEndMem.mli @ 2968

Last change on this file since 2968 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 1.2 KB
RevLine 
[2601]1open Preamble
2
3open Hide
4
5open ByteValues
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
[2649]13open ErrorMessages
14
[2601]15open PreIdentifiers
16
17open Errors
18
19open Lists
20
21open Identifiers
22
23open Integers
24
25open AST
26
27open Division
28
[2717]29open Exp
30
[2601]31open Arithmetic
32
[2773]33open Setoids
34
35open Monad
36
37open Option
38
[2601]39open Extranat
40
41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Positive
48
49open Z
50
51open BitVectorZ
52
53open Pointers
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Extralib
82
83open GenMem
84
[2649]85open Coqlib
86
[2601]87open Values
88
89open FrontEndVal
90
91val loadn :
[2773]92  GenMem.mem -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
[2601]93  Types.option
94
95val load :
[2773]96  AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 Types.option
[2601]97
[2773]98val loadv : AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 Types.option
[2601]99
100val storen :
[2773]101  GenMem.mem -> Pointers.pointer -> ByteValues.beval List.list -> GenMem.mem
102  Types.option
[2601]103
104val store :
[2773]105  AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 -> GenMem.mem
[2601]106  Types.option
107
108val storev :
[2773]109  AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 -> GenMem.mem
[2601]110  Types.option
111
[2773]112val valid_pointer : GenMem.mem -> Pointers.pointer -> Bool.bool
[2601]113
Note: See TracBrowser for help on using the repository browser.