Up – Package index » rocq-runtime » Library rocq-runtime.vernac » ComFixpoint

Module `ComFixpoint`Source

Fixpoints and cofixpoints

Entry points for the vernacular commands Fixpoint and CoFixpoint

val do_mutually_recursive : 
  ?pm:Declare.OblState.t ->
  program_mode:bool ->
  ?use_inference_hook:bool ->
  ?scope:Locality.definition_scope ->
  ?clearbody:bool ->
  kind:Decls.logical_kind ->
  poly:bool ->
  ?typing_flags:Declarations.typing_flags ->
  ?user_warns:Globnames.extended_global_reference UserWarn.with_qf ->
  ?using:Vernacexpr.section_subset_expr ->
  Vernacexpr.recursives_expr ->
  Declare.OblState.t option * Declare.Proof.t option

Internal API

Exported for Funind

Source

val interp_fixpoint_short : 
  Constrexpr.fixpoint_order_expr option list ->
  Vernacexpr.recursive_expr_gen list ->
  Constr.types list * Evd.evar_map