[CakeML-Dev] reusing a CF specification
Michael.Norrish at data61.csiro.au
Michael.Norrish at data61.csiro.au
Fri Oct 14 09:39:19 UTC 2016
I’ve got as far as something like
0. NUM n nv
1. n + 1 < LENGTH a
------------------------------------
cf_app p (Var (Long "Word8" "fromInt")) [Lit (IntLit 0)] (…)
(W8ARRAY av a) (POSTv zv. &WORD 0w zv)
where Word8.fromInt has been declared and characterized by code identical to that in basisProgTheory, but I don’t know how to use the proved specification: xapp throws an exception.
What am I doing wrong?
Many thanks,
Michael.
More information about the Developers
mailing list