helm/ocaml/cic_disambiguation/tests/match.txt

   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
   8 [\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
   9 match (le_n O): le with
  10 [ le_n \Rightarrow (refl_equal nat O)
  11 | (le_S x y) \Rightarrow (refl_equal nat O) ]
  12
  13 (*
  14 [\lambda z:nat. \lambda h:(le 1 z). (le 0 z)]
  15 match (le_S 2 (le_n 1)): le with
  16 [ le_n \Rightarrow (le_S 1 (le_n 0))
  17 | (le_S x y) \Rightarrow y ]
  18 *)
  19
  20 [\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
  21 match (le_S 0 0 (le_n 0)): le with
  22 [ le_n \Rightarrow (le_S 0 0 (le_n 0))
  23 | (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
  24
  25 [\lambda x:bool. nat]
  26 match true:bool with
  27 [ true \Rightarrow O
  28 | false \Rightarrow (S O) ]
  29
  30 [\lambda x:nat. nat]
  31 match O:nat with
  32 [ O \Rightarrow O
  33 | (S x) \Rightarrow (S (S x)) ]
  34
  35 [\lambda x:list. list]
  36 match nil:list with
  37 [ nil \Rightarrow nil
  38 | (cons x y) \Rightarrow (cons x y) ]
  39