helm/software/matita/contribs/ng_assembly2/num/comp_ext.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/comp.ma".
  24 include "common/prod.ma".
  25
  26 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
  27
  28 nrecord comparable_ext : Type[1] ≝
  29  {
  30  comp_base     : comparable;
  31  ltc           : (carr comp_base) → (carr comp_base) → bool;
  32  lec           : (carr comp_base) → (carr comp_base) → bool;
  33  gtc           : (carr comp_base) → (carr comp_base) → bool;
  34  gec           : (carr comp_base) → (carr comp_base) → bool;
  35  andc          : (carr comp_base) → (carr comp_base) → (carr comp_base);
  36  orc           : (carr comp_base) → (carr comp_base) → (carr comp_base);
  37  xorc          : (carr comp_base) → (carr comp_base) → (carr comp_base);
  38  getMSBc       : (carr comp_base) → bool;
  39  setMSBc       : (carr comp_base) → (carr comp_base);
  40  clrMSBc       : (carr comp_base) → (carr comp_base);
  41  getLSBc       : (carr comp_base) → bool;
  42  setLSBc       : (carr comp_base) → (carr comp_base);
  43  clrLSBc       : (carr comp_base) → (carr comp_base);
  44  rcrc          : bool → (carr comp_base) → ProdT bool (carr comp_base);
  45  shrc          : (carr comp_base) → ProdT bool (carr comp_base);
  46  rorc          : (carr comp_base) → (carr comp_base);
  47  rclc          : bool → (carr comp_base) → ProdT bool (carr comp_base);
  48  shlc          : (carr comp_base) → ProdT bool (carr comp_base);
  49  rolc          : (carr comp_base) → (carr comp_base);
  50  notc          : (carr comp_base) → (carr comp_base);
  51  plusc_dc_dc   : bool → (carr comp_base) → (carr comp_base) → ProdT bool (carr comp_base);
  52  plusc_d_dc    : (carr comp_base) → (carr comp_base) → ProdT bool (carr comp_base);
  53  plusc_dc_d    : bool → (carr comp_base) → (carr comp_base) → (carr comp_base);
  54  plusc_d_d     : (carr comp_base) → (carr comp_base) → (carr comp_base);
  55  plusc_dc_c    : bool → (carr comp_base) → (carr comp_base) → bool;
  56  plusc_d_c     : (carr comp_base) → (carr comp_base) → bool;
  57  predc         : (carr comp_base) → (carr comp_base);
  58  succc         : (carr comp_base) → (carr comp_base);
  59  complc        : (carr comp_base) → (carr comp_base);
  60  absc          : (carr comp_base) → (carr comp_base);
  61  inrangec      : (carr comp_base) → (carr comp_base) → (carr comp_base) → bool
  62  }.