blob: 0aa7b5beff577a22509e84802532a21274310d16 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* ============================================== *)
(* To test compilation of dependent case *)
(* Nested patterns *)
(* ============================================== *)
Type <[n:nat]n=n>Cases O of
O => (refl_equal nat O)
| m => (refl_equal nat m)
end.
|
