From Undecidability.L.Tactics Require Import LTactics GenEncode.
Set Default Proof Using "Type".
Section Fix_X.
Variable (X:Type).
Context {intX : registered X}.
MetaCoq Run (tmGenEncode "list_enc" (list X)).
Global Instance termT_cons : computableTime' (@cons X) (fun a aT => (1,fun A AT => (1,tt))).
Proof.
extract constructor.
solverec.
Qed.
End Fix_X.
Hint Resolve list_enc_correct : Lrewrite.
Set Default Proof Using "Type".
Section Fix_X.
Variable (X:Type).
Context {intX : registered X}.
MetaCoq Run (tmGenEncode "list_enc" (list X)).
Global Instance termT_cons : computableTime' (@cons X) (fun a aT => (1,fun A AT => (1,tt))).
Proof.
extract constructor.
solverec.
Qed.
End Fix_X.
Hint Resolve list_enc_correct : Lrewrite.