package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587

Sourcetype t

Sourceval pop : t -> Declare.Proof.t * t option

Sourceval push : t option -> Declare.Proof.t -> t

Sourceval map : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t

Sourceval map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t

Sourceval with_top : t -> f:(Declare.Proof.t -> 'a) -> 'a

Sourceval get_top : t -> Declare.Proof.t