package coq-core

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

A structure S is a non recursive inductive type with a single constructor

module Instance : sig ... end

A canonical instance declares "canonical" conversion hints between the effective components of a structure and the projections of the structure

module ValuePattern : sig ... end

A ValuePattern.t characterizes the form of a component of canonical instance and is used to query the data base of canonical instances

module CanonicalSolution : sig ... end

The canonical solution of a problem (proj,val) is a global constant = fun abs : abstractions_ty => body and body = RecodConstructor params canon_values and the canonical value corresponding to val is val cvalue_arguments. It is possible that val is one of the abs abstractions, eg Default_cs, and in that case cvalue_abstraction = Some i

module CSTable : sig ... end

Low level access to the Canonical Structure database

module PrimitiveProjections : sig ... end

Some extra info for structures which are primitive records

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