Hi all,<div><br></div><div>Ive recently been playing about with abstract blocks and have identified a behaviour that I did not expect.</div><div><br></div><div>Firstly, my understanding of definitions inside an abstract blocks is that when used inside an abstract block they normalise/unfold, and outside of abstract blocks they behave as postulates.</div>
<div><br></div><div>If a non-trivial type is defined as abstract, such as:</div><div><br></div><div><div>abstract</div><div> F : ℕ → Set</div><div> F 0 = ⊤</div><div> F (suc n) = ⊤ × F n</div></div><div><br></div><div>
and then used outside the block in function a definition:</div><div><br></div><div><div>Y : {n : ℕ} → (x : F n) → Set</div><div>Y _ = ⊤</div></div><div><br></div><div>or, concretely:</div><div><br></div><div><div>Z : F 1000 → Set</div>
<div>Z _ = ⊤</div></div><div><br></div><div>lemY : Y {n = 1000} ?</div><div><div><div>lemY = tt</div></div><div><br></div><div>lemZ : Z ?</div><div>lemZ = tt</div><div><br></div></div><div>These two final goals should have the type F 1000, and should not unfold F. But they appear to see through abstract blocks when computing the their types, and judging by the time taken to type-check these definitions suggests that F is being normalised, although only one step reduction is presented in the status window. I.e. after the file has type-checked it will display the goals as (⊤ × F 999).</div>
<div><br></div><div>Notably, should I define:</div><div><br></div><div>abstract</div><div> n1000 = 1000</div><div><br></div><div>postulate A : F n1000</div><div><br></div><div>The term: "Z A" is not accepted when manually checked by C-c,C-d; but is accepted for the goals above.</div>
<div>e.g.</div><div><div>lemZ : Z A</div><div>lemZ = tt</div></div><div><br></div><div>Anyone know if this is this the intended behaviour, or confirm as a bug?</div><div><br></div><div>This occurs in the latest darcs version of Agda.</div>
<div><br></div><div><br></div><div>Thanks,</div><div>Karim Kanso</div><div>Swansea University</div>