translated recursor is axiom-free

coq-community · Jul 30, 2024 · 2aa9842 · 2aa9842
1 parent 044c9e4
commit 2aa9842
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/examples/artifact_paper_example.v b/examples/artifact_paper_example.v
@@ -40,8 +40,6 @@ Proof. trocq. (* replaces N by nat in the goal *) exact nat_rect. Defined.
     the proof of `N_Srec`. The `example` directory of the artifact provides more
     examples, for weaker relations than equivalences, and beyond representation
     independence. *)
-Print N_Srec.
+Set Printing Depth 20.
 Print Assumptions N_Srec.
 
-(* Indeed this computes *)
-Eval compute in N_Srec (fun _ => N) (0%N) N.add 1~0~1~1~0~1%positive.