package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

Sourceval int_or_var : int Locus.or_var Procq.Entry.t

Sourceval nat_or_var : int Locus.or_var Procq.Entry.t

Sourceval pattern_occ : Genredexpr.r_trm Locus.with_occurrences_expr Procq.Entry.t

Sourceval unfold_occ : Genredexpr.r_cst Locus.with_occurrences_expr Procq.Entry.t

val ref_or_pattern_occ : 
  (Genredexpr.r_cst, Genredexpr.r_pat) Util.union Locus.with_occurrences_expr
    Procq.Entry.t

Sourceval occs_nums : Locus.occurrences_expr Procq.Entry.t

Sourceval occs : Locus.occurrences_expr Procq.Entry.t

Sourceval delta_flag : Genredexpr.r_cst Genredexpr.red_atom Procq.Entry.t

Sourceval strategy_flag : Genredexpr.r_cst Genredexpr.glob_red_flag Procq.Entry.t