Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
37d64c87
Commit
37d64c87
authored
Nov 03, 2016
by
Sylvain Dailler
Browse files
Comments on decl_l
parent
d8f8c13e
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/core/trans.mli
View file @
37d64c87
...
...
@@ -58,6 +58,13 @@ val decl : (decl -> decl list ) -> task -> task trans
operation) *)
val
decl_l
:
(
decl
->
decl
list
list
)
->
task
->
task
tlist
(** [decl_l f t1 t2]: on each declaration d of task [t2]
(with [f d] = [ld_1; ld_2; ... ld_n]), create n duplicates (newt_i)
of t1 with the declaration d_i replaced by ld_i.
Note for example that this 'decl_l (fun d -> [[d]; [d]])' will
duplicate the task on each declaration and probably run forever.
*)
val
tdecl
:
(
decl
->
tdecl
list
)
->
task
->
task
trans
val
tdecl_l
:
(
decl
->
tdecl
list
list
)
->
task
->
task
tlist
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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