File: bug_10031.v

package info (click to toggle)
coq 9.1.0%2Bdfsg-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 35,964 kB
  • sloc: ml: 239,908; sh: 4,355; python: 2,985; ansic: 2,644; makefile: 874; lisp: 171; javascript: 63; xml: 24; sed: 2
file content (9 lines) | stat: -rw-r--r-- 591 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
 
Require Import BinNums PrimInt63 Uint63Axioms.

Open Scope uint63_scope.

Goal False.
cut (let (q, r) := (0, 0) in (to_Z q, to_Z r) = ((Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (* 9223372036854775808%Z *), Z0));
  [discriminate| ].
Fail (change (0, 0) with (diveucl_21 1 0 1); apply diveucl_21_spec).
Abort.