Module FixTacticsSource

Fixpoint and co-fixpoint tactics.

Sourceval 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).
Sourceval 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.

cofix f refines the goal using a cofixpoint.

  • f is the name of the variable which represents the cofixpoint.
Sourceval 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.