Is there a way to print a term as Coq would accept as input? I thought
Inductive tree : Set := node : A -> forest -> tree with forest : Set := leaf : B -> forest | cons : tree -> forest -> forest. Scheme tree_forest_rec := Induction for tree Sort Set with forest_tree_rec := Induction for forest Sort Set. Print tree_forest_rec.
When I copy and paste the printed term with Coq 8.13.1, I get the following error:
Error: Syntax error: [term level 200] expected after '=>' (in [binder_constr]).
Below is the printed term:
tree_forest_rec = fun (P : tree -> Set) (P0 : forest -> Set) (f : forall (a : A) (f : forest), P0 f -> P (node a f)) (f0 : forall b : B, P0 (leaf b)) (f1 : forall t : tree, P t -> forall f1 : forest, P0 f1 -> P0 (cons t f1)) => with F (t : tree) : P t := match t as t0 return (P t0) with | node a f2 => f a f2 (F0 f2) end with F0 (f2 : forest) : P0 f2 := match f2 as f3 return (P0 f3) with | leaf b => f0 b | cons t f3 => f1 t (F t) f3 (F0 f3) end for F : forall (P : tree -> Set) (P0 : forest -> Set), (forall (a : A) (f : forest), P0 f -> P (node a f)) -> (forall b : B, P0 (leaf b)) -> (forall t : tree, P t -> forall f1 : forest, P0 f1 -> P0 (cons t f1)) -> forall t : tree, P t
hmm, I guess it is a printing bug in the case of mutually recursive functions
Yes, that's a bug, if should not start with
Indeed, that's a bug, please open a report. As of today it should be noted that in general, printing Coq programs won't produce output that can be parsed _and interpreted_ back; this is due to a complex set of issues, and may be hard to fix, but in particular printing is not injective w.r.t. AST.
Depending on the needs of your use case, you could be better off with actually using a faithful representation of the AST such as the one provided by SerAPI.
Last updated: Sep 26 2023 at 12:02 UTC