package GuaCaml

  1. Overview
  2. Docs
package GuaCaml
Legend:
Library
Module
Module type
Parameter
Class
Class type
type (!'a, !'d) proof =
  1. | End
  2. | Seq of 'a list * ('a, 'd) proof
  3. | Sum of 'd * ('a, 'd) proof list
val proof_normalize : ('a, 'b) proof -> ('a, 'b) proof
type (!'a, !'d, !'s, !'c) pproof =
  1. | PEnd
  2. | PNxt of 's
  3. | PSeq of 'a list * 'c * 's * ('a, 'd, 's, 'c) pproof
  4. | PSum of 'd * 'c * ('s * ('a, 'd, 's, 'c) pproof) list
  5. | PMin of 's * ('a, 'd, 's, 'c) pproof list
val pproof_normalize : ('a -> 'a -> 'a) -> ('b, 'c, 'd, 'a) pproof -> ('b, 'c, 'd, 'a) pproof
type (!'a, !'d) aproof =
  1. | AEnd
  2. | ANxt
  3. | ASeq of 'a list
  4. | ASum of 'd
  5. | AMin
val aproof_of_pproof : ('a, 'b, 'c, 'd) pproof -> ('a, 'b) aproof
val proof_of_pproof : ('a, 'd, 's, 'c) pproof -> ('a, 'd) proof
val cost_of_pproof : (unit -> 'c) -> ('c -> 'c -> 'c) -> ('s -> 'c) -> ('a, 'd, 's, 'c) pproof -> 'c
module ToS : sig ... end
module type MSig = sig ... end
module MakeProfile (H : MSig) : sig ... end
module type Sig = sig ... end
module Make (H0 : MSig) : sig ... end