Inductive nat: Set := O: nat | S: nat -> nat.

Definition x := S (S (S O)).

Print x.

(* Recursively define plus. *)

Fixpoint my_plus (u: nat) (v: nat) :=

match u with

| O => v

| S(u') => S(my_plus u' v)

end.

Compute my_plus S(S(O)) S(O).

when executed to the last line, the coqide shows the "coqidetop died badly." error.

Any help is appreciated, thanks in advance!

Some more information is required. The following does work for me (with Coq/CoqIDE 8.13.2, but very likely also with previous versions):

```
Inductive nat: Set := O: nat | S: nat -> nat.
Definition x := S (S (S O)).
Print x.
(* Recursively define plus. *)
Fixpoint my_plus (u: nat) (v: nat) :=
match u with
| O => v
| S(u') => S(my_plus u' v)
end.
Compute my_plus (S(S O)) (S O).
```

Note that `Compute my_plus S(S(O)) S(O)`

without outer parenthesis does not parse in a usual environment, so I guess you are doing something slightly different than you wrote. In Coq parenthesis are not used as function call operators, but to group terms. So `f`

applied to `x`

is written just `f x`

or `(f x)`

. `f (x)`

is also valid - a redundant pair of parenthesis around x, but a bit confusing.

You would get a stack overflow if you use very large Peano (non binary) numbers:

```
Require Import Nat.
Compute (pow 2 15). (* Works *)
Compute (pow 2 16). (* Stack overflow *)
```

but this is explicitly a stack overflow and not a "Coqtop died badly", but that might have been different in older versions.

The `Coqtop died badly`

is more commonly a configuration issue - things like using file names or paths which are not valid Coq module names, but then you would get an error earlier.

OK, I see this is already solved in a double posted thread.

@zhengyu shi : in the future please avoid to post the same question twice.

Last updated: Feb 04 2023 at 22:29 UTC