diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-21 01:43:10 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-21 09:29:26 +0100 |
commit | 9c2662eecc398f38be3b6280a8f760cc439bc31c (patch) | |
tree | 497b1c250e3cb2e918982b25bb029c14603ac96f /lib/cList.mli | |
parent | 4b075af747f65bcd73ff1c78417cf77edf6fbd76 (diff) |
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
Diffstat (limited to 'lib/cList.mli')
-rw-r--r-- | lib/cList.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/cList.mli b/lib/cList.mli index 1487f67a3..9c7b815c1 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -94,6 +94,9 @@ sig (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i [f ai = true], then [smartfilter f l == l] *) + val extend : bool list -> 'a -> 'a list -> 'a list +(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n]; + it extends [a1..an] by inserting [a] at the position of [false] in [l] *) val count : ('a -> bool) -> 'a list -> int val index : 'a eq -> 'a -> 'a list -> int |