Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
menhir
Commits
f1c63061
Commit
f1c63061
authored
Jul 03, 2015
by
POTTIER Francois
Browse files
Added [min_cutoff].
parent
0c058ae9
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/CompletedNatWitness.ml
View file @
f1c63061
...
...
@@ -48,6 +48,17 @@ let min_lazy p1 p2 =
|
_
->
min
p1
(
p2
()
)
let
min_cutoff
p1
p2
=
match
p1
with
|
Finite
(
0
,
_
)
->
p1
|
Finite
(
i1
,
_
)
->
(* Pass [i1] as a cutoff value to [p2]. *)
min
p1
(
p2
i1
)
|
Infinity
->
(* Pass [max_int] to indicate no cutoff. *)
p2
max_int
(* [until_finite] can be viewed as a variant of [min_lazy] where
we are happy as soon as we find a finite value. It can be viewed
as a minimum operation for the partial ordering where [Infinity]
...
...
src/CompletedNatWitness.mli
View file @
f1c63061
...
...
@@ -21,6 +21,8 @@ val add: 'a t -> 'a t -> 'a t
val
min_lazy
:
'
a
t
->
(
unit
->
'
a
t
)
->
'
a
t
val
add_lazy
:
'
a
t
->
(
unit
->
'
a
t
)
->
'
a
t
val
min_cutoff
:
'
a
t
->
(
int
->
'
a
t
)
->
'
a
t
val
until_finite
:
'
a
t
->
(
unit
->
'
a
t
)
->
'
a
t
val
print
:
(
'
a
->
string
)
->
'
a
t
->
string
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment