오류 : COQ

Question

내가 Mem.load을 전개하기 위해 노력하고있어에서 평가 가능한 기준을 강요 할 수 없습니다 나는 오류를 얻을 :

Error: Cannot coerce Mem.load to an evaluable reference.

내가 load1로 Mem.load의 동일한 Definition을 쓰고 unfoldable입니다. 이것은 그것이 unfold ED 수 없음을 의미

Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes. 

:

Require Import compcert.common.AST. 
Require Import compcert.common.Memory. 
Require Import compcert.common.Values. 
Require Import compcert.lib.Coqlib. 
Require Import compcert.lib.Maps. 

Local Notation "a # b" := (PMap.get b a) (at level 1). 

Definition load1 (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val := 
    if Mem.valid_access_dec m chunk b ofs Readable 
    then Some(decode_val chunk (Mem.getN (size_chunk_nat chunk) ofs (m.(Mem.mem_contents)#b))) 
    else None. 

Lemma mem_load_eq: forall (c : memory_chunk) (m : mem) (b : block) (ofs : Z), 
(load1 c m b ofs) = (Mem.load c m b ofs). 
Proof. 
    intros. 
    unfold load1. 
    unfold Mem.load. (*I get error here when unfolding *) 
Admitted. 

Answer 1

compcert.common.Memory 모듈 불투명 할 Mem.load 등 여러 이름을 정의한다. unfold Mem.load하기 전에

그냥 모든 작동 후에는 Transparent이라고 말할 :

Transparent Mem.load. 
unfold Mem.load.