## Stream: Coq users

#### leafGecko (Apr 24 2021 at 09:54):

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!

#### Michael Soegtrop (Apr 25 2021 at 08:09):

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.

#### Michael Soegtrop (Apr 25 2021 at 08:15):

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

#### Michael Soegtrop (Apr 25 2021 at 08:16):

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

Last updated: Jun 13 2024 at 08:02 UTC