blob: d3c0410ea5470110dbc33b0df244b05c5f5d4701 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Require Export NumPrelude.
Require Export NZAxioms.
Set Implicit Arguments.
Module Type ZAxiomsSig.
Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
Open Local Scope NatIntScope.
Notation Z := NZ (only parsing).
Notation E := NZE (only parsing).
(** Integers are obtained by postulating that every number has a predecessor *)
Axiom S_P : forall n : Z, S (P n) == n.
End ZAxiomsSig.
(*
Local Variables:
tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
End:
*)
|
