package coq

You can search for identifiers within the package.

in-package search v0.2.0

Module `Derive_plugin.Derive`Source

val start_deriving : 
  Names.Id.t ->
  Constrexpr.constr_expr ->
  Names.Id.t ->
  Declare.Proof.t

start_deriving f suchthat lemma starts a proof of suchthat (which can contain references to f) in the context extended by f:=?x. When the proof ends, f is defined as the value of ?x and lemma as the proof.

package coq

Module Derive_plugin.DeriveSource

Module `Derive_plugin.Derive`Source