Hi!

Is there a way to print a term as Coq would accept as input? I thought `Print`

would do, but it fails on the the generated scheme for trees and forests, as described in the documentation (https://coq.inria.fr/distrib/current/refman/user-extensions/proof-schemes.html?highlight=scheme):

```
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 `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: May 25 2024 at 20:01 UTC