leafGecko (Apr 24 2021 at 09:54): 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 fapplied 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: Oct 13 2024 at 01:02 UTC