I'm trying to define a type for arbitrary terms (for universal algebra) and got stuck with the positivity checker.

The following is allowed.

```
From Coq Require Import Vector.
Inductive tree :=
| tree_ctr (n : nat) (branch : Vector.t tree n).
```

But the following, which I'd like to do, is not.

```
Fixpoint Power (A : Type) (n : nat) : Type :=
match n with
| O => unit
| S n =>
A * Power A n
end.
Fail Inductive tree :=
| tree_ctr (n : nat) (branch : Power tree n).
```

And for some reason it is permitted to use `Power`

if `n`

is constant.

```
Inductive tree :=
| tree_ctr (branch : Power tree 5).
```

I'm not sure what the problem is, because `Power`

and `Vector.t`

have the same type. Is there some reason for this behavior and/or some workaround?

Found Issue 1433 mentioning this. It seems that this is currently not possible. I think I'll go with the `Vector`

based solution and use the natural bijection between `Vector.t A n`

and `Power A n`

to transform between them.

Stéphane Desarzens has marked this topic as resolved.

Last updated: Jun 25 2024 at 18:02 UTC