package GuaCaml

  1. Overview
  2. Docs
package GuaCaml
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a proof = 'a list
type (!'a, !'s, !'c) pproof =
  1. | PEnd
  2. | PNxt of 's
  3. | PSeq of 'a list * 'c * 's * ('a, 's, 'c) pproof
  4. | PMin of 's * ('a, 's, 'c) pproof list
val pproof_normalize : ('a -> 'a -> 'a) -> ('b, 'c, 'a) pproof -> ('b, 'c, 'a) pproof
type !'a aproof =
  1. | AEnd
  2. | ANxt
  3. | ASeq of 'a list
  4. | AMin
val aproof_of_pproof : ('a, 'b, 'c) pproof -> 'a aproof
module type MSig = sig ... end
module type Sig = sig ... end
module Make (H0 : MSig) : sig ... end