[Agda] test report

[mechvel at scico.botik.ru]

On 2021-03-15 13:01, Nils Anders Danielsson wrote:
> On 2021-03-14 23:47, mechvel at scico.botik.ru wrote:
>> * I failed to separate the proof.
> 
> I suggest that you try to mark the proof parts with @0, so that they 
> are
> erased by the compiler:
> 
>   
> https://agda.readthedocs.io/en/latest/language/runtime-irrelevance.html


I have

efficient-withProof : Pol → Σ Pol (\h -> h =ₚ simple f)
-- The proper result and the proof
-- for its equality to the result of the simple method.
-- There are ready the needed proofs for `simple', and they will be 
ported
-- to `efficient' by using the proof part in efficient-withProof.
-- (For `simple' proofs are simpler to build).

efficient-withProof f =
   case foo f
   of \
   { (no ¬hm) → let 0=simple-f =  simple-¬hm=0 f ¬hm
                in  (0ₚ , 0=simple-f)
    ;  ...
       has complex recursions
   }

efficient : Pol -> Pol
efficient = proj₁ ∘ efficient-withProof

efficient-P : (f : Pol) -> P (efficient f)              -- usage
efficient-P f =
           let (h , h=simple-f) = efficient-withProof f
           in
           P-cong (simple-P f) (=sym h=simple-f)

P (efficient f)  is derived from  h=simple-f  derived here and
from  simple-P, P-cong  proved earlier.


I tried to insert @0 to various places in  efficient-withProof  
signature and body,
and it reports "Parse error".

Is @0 (@erased) a language construct or it is a function to be imported 
from somewhere?

Thanks,

--
SM