blob: cf06eaf58fd76871885294c5377b9710dc1d5a31 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
(* TEST
* expect
*)
type _ nat =
Zero : [`Zero] nat
| Succ : 'a nat -> [`Succ of 'a] nat;;
type 'a pre_nat = [`Zero | `Succ of 'a];;
type aux =
| Aux : [`Succ of [<[<[<[`Zero] pre_nat] pre_nat] pre_nat]] nat -> aux;;
let f (Aux x) =
match x with
| Succ Zero -> "1"
| Succ (Succ Zero) -> "2"
| Succ (Succ (Succ Zero)) -> "3"
| Succ (Succ (Succ (Succ Zero))) -> "4"
| _ -> . (* error *)
;;
[%%expect{|
type _ nat = Zero : [ `Zero ] nat | Succ : 'a nat -> [ `Succ of 'a ] nat
type 'a pre_nat = [ `Succ of 'a | `Zero ]
type aux =
Aux :
[ `Succ of [< [< [< [ `Zero ] pre_nat ] pre_nat ] pre_nat ] ] nat ->
aux
Line 14, characters 4-5:
14 | | _ -> . (* error *)
^
Error: This match case could not be refuted.
Here is an example of a value that would reach it:
Succ (Succ (Succ (Succ (Succ Zero))))
|}];;
|
