You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The following code displays correctly for small values of fib (up to 11) and breaks starting at (12). What breaks is that the goal window is empty. Normal behavoir can only by restored by entering "Developer:Reload Window".
Require Import List Reals.
Open Scope R_scope.
Definition fib_aux :=
nat_rect (fun _ => list R) (0 :: 1 :: nil)
(fun _ v => (nth 1 v 0 :: nth 0 v 0 + nth 1 v 0 :: nil))
.
Definition fib (n : nat) : R :=
nth 0 (fib_aux n) 0.
Lemma big_fib : fib 12 = 10.
Proof.
unfold fib; simpl.
The text was updated successfully, but these errors were encountered:
The following code displays correctly for small values of fib (up to 11) and breaks starting at (12). What breaks is that the goal window is empty. Normal behavoir can only by restored by entering "Developer:Reload Window".
The text was updated successfully, but these errors were encountered: