Module FixTactics

Fixpoint and co-fixpoint tactics.

val fix : Names.Id.t -> int -> unit Proofview.tactic

fix f idx refines the goal using a fixpoint.

  • f is the name of the variable which represents the fixpoint.
  • idx is the index of the structurally recursive argument (starting at 1).
val mutual_fix : Names.Id.t -> int -> (Names.Id.t * int * EConstr.constr) list -> unit Proofview.tactic

mutual_fix f idx fs refines the goal using a mutual fixpoint.

  • f and idx are the name and recursive argument index for the first fixpoint. The type of f is simply the conclusion of the goal.
  • fs contains the name, recursive argument index, and type of every other fixpoint in the mutual block.
val cofix : Names.Id.t -> unit Proofview.tactic

cofix f refines the goal using a cofixpoint.

  • f is the name of the variable which represents the cofixpoint.
val mutual_cofix : Names.Id.t -> (Names.Id.t * EConstr.constr) list -> unit Proofview.tactic

mutual_cofix f fs refines the goal using a mutual cofixpoint.

  • f is the name of the first cofixpoint. The type of f is simply the conclusion of the goal.
  • fs contains the name and type of every other cofixpoint in the mutual block.