Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Ortac_runtime_qcheck_stm.Z
Sourceexists i j p
is true
iff the predicate there exists k
within i
and j
, included, for which p
holds.