next up previous contents
Next: Basic Lemmas Up: The Integers Previous: Extra lemmas for integers

The Integers--Definitions

In this file are given some basic definitions for the integers. The datatype itself, its equality, various constants and some operations are defined. The internal sigma-type is used to define the pairs of integers. This is mainly because using inductive cross-product is slower to run.

 ** Module lib_int_basics Imports lib_int_nat_lemmas lib_nat_minus_thms
     lib_sets_ccmj
  zed = ... : Type
  Eq_zed = ... : zed->zed->Prop
  Eq_refl_zed = ... : refl Eq_zed
  Eq_sym_zed = ... : sym Eq_zed
  Eq_trans_zed = ... : trans Eq_zed
  int = ... : set
  zero_zed = ... : int.1
  one_zed = ... : int.1
  two_zed = ... : int.1
  three_zed = ... : int.1
  four_zed = ... : int.1
  minus_one_zed = ... : int.1
  plus_zed = ... : int.1->int.1->int.1
  times_zed = ... : int.1->int.1->int.1
  minus_zed = ... : int.1->int.1->int.1
  neg_zed = ... : int.1->int.1



Lego
1998-06-15