blob: db25ce7302661e59ad1fb9ec3819464901e84f0a (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
open Pcaml
(** * Non-irrefutable patterns
This small camlp4 extension creates a "let*" variant of the "let"
syntax that allow the use of a non-exhaustive pattern. The typical
usage is:
let* x::l = foo in ...
when foo is already known to be non-empty. This way, no warnings by ocamlc.
A Failure is raised if the pattern doesn't match the expression.
*)
EXTEND
expr:
[[ "let"; "*"; p = patt; "="; e1 = expr; "in"; e2 = expr ->
<:expr< match $e1$ with
[ $p$ -> $e2$
| _ -> failwith "Refutable pattern failed"
] >> ]];
END
|
