package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Finding subterms, possibly up to some unification function, possibly at some given occurrences

exception NotUnifiable of (EConstr.constr * EConstr.constr * Pretype_errors.unification_error) option
exception SubtermUnificationError of Pretype_errors.subterm_unification_error

A testing function is typically a unification function returning a substitution or failing with a NotUnifiable error, together with a function to merge substitutions and an initial substitution; last_found is used for error messages and it has to be initialized with None.

type 'a testing_function = {
  1. match_fun : 'a -> EConstr.constr -> 'a;
  2. merge_fun : 'a -> 'a -> 'a;
  3. mutable testing_state : 'a;
  4. mutable last_found : Pretype_errors.position_reporting option;
}

This is the basic testing function, looking for exact matches of a closed term

replace_term_occ_modulo occl test mk c looks in c for subterm modulo a testing function test and replaces successfully matching subterms at the indicated occurrences occl with mk (); it turns a NotUnifiable exception raised by the testing function into a SubtermUnificationError.

replace_term_occ_decl_modulo is similar to replace_term_occ_modulo but for a named_declaration.

subst_closed_term_occ occl c d replaces occurrences of closed c at positions occl by Rel 1 in d (see also Note OCC), unifying universes which results in a set of constraints.

subst_closed_term_occ_decl evd occl c decl replaces occurrences of closed c at positions occl by Rel 1 in decl.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct