Hello.

About half year ago code below worked

```
Inductive even : nat -> Type :=
| EZ : even 0
| ES : forall n, odd n -> even (S n)
with odd : nat -> Type :=
| OS : forall n, even n -> odd (S n).
Fixpoint even_sum n1 n2 (e1 : even n1) : even n2 -> even (n1 + n2) :=
match e1 with
| EZ => fun e2 => e2
| ES _ o1 => fun e2 => ES (odd_sum o1 e2)
end
with odd_sum n1 n2 (o : odd n1) : even n2 -> odd (n1 + n2) :=
match o with
| OS _ e => fun e2 => OS (even_sum e e2)
end.
```

Now it gives me next error:

```
Error:
In environment
even_sum : forall n1 n2 : nat, even n1 -> even n2 -> even (n1 + n2)
odd_sum : forall n1 n2 : nat, odd n1 -> even n2 -> odd (n1 + n2)
n1 : nat
n2 : nat
e1 : even n1
e2 : even n2
The term "e2" has type "even n2" while it is expected to have type "even (?n@{n0:=0} + n2)".
```

As I see, it is not able to compute that 0 + n2 is n2 anymore (but i'm not sure why it says about n0 instead of n...).

How to fix?

Maybe there is something about implicit arguments, but at least (with explicit arguments) the following seems to work:

```
Fixpoint even_sum n1 n2 (e1 : even n1) : even n2 -> even (n1 + n2) :=
match e1 with
| EZ => fun e2 => e2
| ES _ o1 => fun e2 => ES _ (odd_sum _ _ o1 e2)
end
with odd_sum n1 n2 (o : odd n1) : even n2 -> odd (n1 + n2) :=
match o with
| OS _ e => fun e2 => OS _ (even_sum _ _ e e2)
end.
```

and with implicit arguments:

```
Set Implicit Arguments.
Inductive even : nat -> Type :=
| EZ : even 0
| ES : forall n, odd n -> even (S n)
with odd : nat -> Type :=
| OS : forall n, even n -> odd (S n).
Fixpoint even_sum n1 n2 (e1 : even n1) : even n2 -> even (n1 + n2) :=
match e1 with
| EZ => fun e2 => e2
| ES o1 => fun e2 => ES (odd_sum o1 e2)
end
with odd_sum n1 n2 (o : odd n1) : even n2 -> odd (n1 + n2) :=
match o with
| OS e => fun e2 => OS (even_sum e e2)
end.
```

Thank you. I think I forgot about Set Implicit Arguments or something like.

Andrey Klaus has marked this topic as resolved.

Last updated: May 18 2024 at 10:02 UTC