DIGEST 693b57d74f776ae8bd215fbfc8b03df3
Fmem_metadata
R15:23 Sail.Base <> <> lib
def 52:60 <> write_ram
binder 63:64 <> rv:1
binder 66:66 <> e:2
binder 68:68 <> a:3
binder 71:72 <> wk:4
R82:86 Sail.Values <> mword def
R88:88 mem_metadata <> a:3 var
binder 75:78 <> addr:5
binder 91:94 <> size:6
R101:105 Sail.Values <> mword def
R109:111 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R112:115 mem_metadata <> size:6 var
binder 97:97 <> v:7
R127:130 Coq.Init.Datatypes <> unit ind
binder 120:123 <> meta:8
R135:139 Sail.Prompt_monad <> monad ind
R141:142 mem_metadata <> rv:1 var
R144:147 Coq.Init.Datatypes <> bool ind
R149:149 mem_metadata <> e:2 var
R154:162 Sail.Prompt_monad <> write_mem def
R179:179 mem_metadata <> v:7 var
R174:177 mem_metadata <> size:6 var
R169:172 mem_metadata <> addr:5 var
R167:167 mem_metadata <> a:3 var
R164:165 mem_metadata <> wk:4 var
def 194:201 <> read_ram
binder 204:205 <> rv:9
binder 207:207 <> e:10
binder 209:209 <> a:11
binder 212:213 <> rk:12
R223:227 Sail.Values <> mword def
R229:229 mem_metadata <> a:11 var
binder 216:219 <> addr:13
binder 232:235 <> size:14
R249:252 Coq.Init.Datatypes <> bool ind
binder 238:245 <> read_tag:15
R257:265 Sail.Values <> ArithFact class
R272:276 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R268:271 mem_metadata <> size:14 var
binder 257:278 <> H:16
R283:287 Sail.Prompt_monad <> monad ind
R289:290 mem_metadata <> rv:9 var
R309:311 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
R293:297 Sail.Values <> mword def
R301:303 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R304:307 mem_metadata <> size:14 var
R312:315 Coq.Init.Datatypes <> unit ind
R318:318 mem_metadata <> e:10 var
R348:352 Sail.Prompt_monad <> :::x_'>>='_x not
R325:332 Sail.Prompt_monad <> read_mem def
R344:347 mem_metadata <> size:14 var
R339:342 mem_metadata <> addr:13 var
R337:337 mem_metadata <> a:11 var
R334:335 mem_metadata <> rk:12 var
binder 357:360 <> data:17
R367:373 Sail.Prompt_monad <> returnm def
R375:375 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R380:381 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R384:384 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R376:379 mem_metadata <> data:17 var
R382:383 Coq.Init.Datatypes <> tt constr