[isabelle] export_code ... checking



Dear code export experts,

do I assume correctly that

  export_code f1 ... fN checking

can be used to "check" whether code generation "works" (at least to some extend) for constants f1 ... fN. If so, is it an unofficial feature that shouldn't be used in production code?

cheers

chris




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.