helm/gTopLevel/tests/match05.cic.test

   1 [\lambda x:list. list]
   2 match nil:list with
   3 [ nil \Rightarrow nil
   4 | (cons x y) \Rightarrow (cons x y) ]
   5 ###### INTERPRETATION NUMBER 1 ######
   6 ### (* disambiguation environment  *)
   7 alias id cons = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1/2)
   8 alias id list = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1)
   9 alias id nil = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1/1)
  10 ### (* METASENV after disambiguation  *)
  11 _ :? _; _ :? _ |- ?25: Type
  12 ### (* TERM after disambiguation      *)
  13
  14 <[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of
  15  nil => nil{A:=?25[_ ; _]}
  16  cons => [x:?25[_ ; _]][y:list{A:=?25[_ ; x]}](cons{A:=?25[x ; y]} x y)
  17 end
  18 ### (* TYPE_OF the disambiguated term *)
  19 ([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
  20 ### (* REDUCED disambiguated term     *)
  21 nil{A:=?25[_ ; _]}
  22 ###### INTERPRETATION NUMBER 2 ######
  23 ### (* disambiguation environment  *)
  24 alias id cons = cic:/Coq/Lists/List/list.ind#xpointer(1/1/2)
  25 alias id list = cic:/Coq/Lists/List/list.ind#xpointer(1/1)
  26 alias id nil = cic:/Coq/Lists/List/list.ind#xpointer(1/1/1)
  27 ### (* METASENV after disambiguation  *)
  28 _ :? _; _ :? _ |- ?25: Set
  29 ### (* TERM after disambiguation      *)
  30
  31 <[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of
  32  nil => nil{A:=?25[_ ; _]}
  33  cons => [x:?25[_ ; _]][y:list{A:=?25[_ ; x]}](cons{A:=?25[x ; y]} x y)
  34 end
  35 ### (* TYPE_OF the disambiguated term *)
  36 ([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
  37 ### (* REDUCED disambiguated term     *)
  38 nil{A:=?25[_ ; _]}
  39 ###### INTERPRETATION NUMBER 3 ######
  40 ### (* disambiguation environment  *)
  41 alias id cons = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1/2)
  42 alias id list = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1)
  43 alias id nil = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1/1)
  44 ### (* METASENV after disambiguation  *)
  45
  46 ### (* TERM after disambiguation      *)
  47
  48 <[x:list]list>Cases nil of
  49  nil => nil
  50  cons => [x:A][y:list](cons x y)
  51 end
  52 ### (* TYPE_OF the disambiguated term *)
  53 ([x:list]list nil)
  54 ### (* REDUCED disambiguated term     *)
  55 nil
  56 ###### INTERPRETATION NUMBER 4 ######
  57 ### (* disambiguation environment  *)
  58 alias id cons = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1/2)
  59 alias id list = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1)
  60 alias id nil = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1/1)
  61 ### (* METASENV after disambiguation  *)
  62 _ :? _; _ :? _ |- ?25: Set
  63 ### (* TERM after disambiguation      *)
  64
  65 <[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of
  66  nil => nil{A:=?25[_ ; _]}
  67  cons => [x:?25[_ ; _]][y:list{A:=?25[_ ; x]}](cons{A:=?25[x ; y]} x y)
  68 end
  69 ### (* TYPE_OF the disambiguated term *)
  70 ([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
  71 ### (* REDUCED disambiguated term     *)
  72 nil{A:=?25[_ ; _]}