helm/gTopLevel/tests/match00.cic.test

   1 [\lambda x:nat.
   2   [\lambda y:nat. Set]
   3     match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
   4 match (S O):nat with
   5 [ O \Rightarrow O
   6 | (S x) \Rightarrow false ]
   7 ###### INTERPRETATION NUMBER 1 ######
   8 ### (* disambiguation environment  *)
   9 alias id O = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)
  10 alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
  11 alias id bool = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)
  12 alias id false = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)
  13 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
  14 ### (* METASENV after disambiguation  *)
  15
  16 ### (* TERM after disambiguation      *)
  17
  18 <[x:nat]
  19 <[y:nat]Set>Cases x of
  20  O => nat
  21  S => [x:nat]bool
  22 end>Cases (S O) of
  23  O => O
  24  S => [x:nat]false
  25 end
  26 ### (* TYPE_OF the disambiguated term *)
  27 ([x:nat]
  28 <[y:nat]Set>Cases x of
  29  O => nat
  30  S => [x:nat]bool
  31 end (S O))
  32 ### (* REDUCED disambiguated term     *)
  33 false