This add new term constructors to map to lazy and force in ocaml/malfunction or more naive thunks in other targets.
This is now used in the unverified ECoInductiveToInductive phase. In coq-malfunction we can compile this to ocaml's implementation for an efficient implementation of coinductives and cofixpoints.
As these constructors are not produced by erasure, and we do NOT add evaluation rules for lazy/force, the correctness proofs do not change for the rest of the pipeline. It should just be considered unsafe to use lazy and force.
This add new term constructors to map to lazy and force in ocaml/malfunction or more naive thunks in other targets. This is now used in the unverified ECoInductiveToInductive phase. In coq-malfunction we can compile this to ocaml's implementation for an efficient implementation of coinductives and cofixpoints.
As these constructors are not produced by erasure, and we do NOT add evaluation rules for lazy/force, the correctness proofs do not change for the rest of the pipeline. It should just be considered unsafe to use lazy and force.