blob: 4f0470b1df6a45c3ee36c3ff0a2237ec6e08e6b0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *)
Require Import ZArith.
Require Recdef.
Axiom nat_eq_dec: forall x y : nat, {x=y}+{x<>y}.
Locate eq_sym. (* Constant Coq.Init.Logic.eq_sym *)
Function loop (n: nat) {measure (fun x => x) n} : bool :=
if nat_eq_dec n 0 then false else loop (pred n).
Proof.
admit.
Defined.
Check eq_sym eq_refl : 0=0.
|
