package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.tactics/FixTactics/index.html

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.