97 open Hints_declaration
119 val check_well_cost_fn : RTLabs_syntax.internal_function -> Bool.bool
123 val check_label_bounded :
124 RTLabs_syntax.statement Graphs.graph -> Graphs.label -> Graphs.label
125 List.list -> Identifiers.identifier_set -> Nat.nat ->
126 Identifiers.identifier_set Types.option
128 val check_graph_bounded :
129 RTLabs_syntax.statement Graphs.graph -> Identifiers.identifier_set ->
130 Graphs.label -> Nat.nat -> Bool.bool
132 val check_sound_cost_fn : RTLabs_syntax.internal_function -> Bool.bool
134 val check_cost_program : RTLabs_syntax.rTLabs_program -> Bool.bool
136 val check_cost_program_prf : RTLabs_syntax.rTLabs_program -> __ Errors.res