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 [\lambda z:nat. \lambda h:(le (plus (plus O O) (plus O O)) z). (eq nat (plus (plus O O) (plus O O)) (plus (plus O O) (plus O O)))]
  14 match (le_n (plus (plus O O) (plus O O))): le with
  15 [ le_n \Rightarrow (refl_equal nat (plus (plus O O) (plus O O)))
  16 | (le_S x y) \Rightarrow (refl_equal nat (plus (plus O O) (plus O O))) ]
  17
  18 (*
  19 [\lambda z:nat. \lambda h:(le 1 z). (le 0 z)]
  20 match (le_S 2 (le_n 1)): le with
  21 [ le_n \Rightarrow (le_S 1 (le_n 0))
  22 | (le_S x y) \Rightarrow y ]
  23 *)
  24
  25 [\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
  26 match (le_S 0 0 (le_n 0)): le with
  27 [ le_n \Rightarrow (le_S 0 0 (le_n 0))
  28 | (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
  29
  30
  31 [\lambda x:bool. nat]
  32 match true:bool with
  33 [ true \Rightarrow O
  34 | false \Rightarrow (S O) ]
  35
  36 [\lambda x:nat. nat]
  37 match O:nat with
  38 [ O \Rightarrow O
  39 | (S x) \Rightarrow (S (S x)) ]
  40
  41 [\lambda x:list. list]
  42 match nil:list with
  43 [ nil \Rightarrow nil
  44 | (cons x y) \Rightarrow (cons x y) ]
  45
  46 \lambda x:False.
  47   [\lambda h:False. True]
  48   match x:False with []
  49