package coq-core

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

telescope env sigma ctx turns a context x1:A1;...;xn:An into a right-associated nested sigma-type of the right sort. It returns:

  • the nested sigma-type T := {x1:A1 & ... {xn-1:An-1 & ... An} ... }
  • the canonical tuple (existsT _ x1 ... (existsT _ xn-1 xn) ...) inhabiting the sigma-type in the given context
  • an instantiation of the assumptions of ctx with values they have in the context x:T, that is x1:=projT1 x;...;xn-1:=projT1 ... (projT2 x);xn:=projT2 ... (projT2 x); note that let-ins in the original context are preserved Depending on the sorts of types, it uses either ex, sig or sigT, even if we always used sigT above as an example.
type telescope = {
  1. telescope_type : EConstr.types;
  2. telescope_value : EConstr.constr;
}

make_iterated_tuple env sigma ~default c encapsulates c (of inferred type C) and its free variables x1,...,xn into a right-associated nested tuple in a sigT-type. It returns:

  • the nested type {x1:A1 & ... {xn:An & ... C} ... }
  • the tuple (existsT _ x1 ... (existsT _ xn c) ...)
  • an alternative tuple (existsT _ x1 ... (existsT _ xn default) ...); if default has not the right type, it fails.

make_selector env sigma ~pos ~special ~default c constructs a case-split on c (assumed of inductive type), with the pos-th branch returning special, and all the other branch returning default.

val make_selector : Environ.env -> Evd.evar_map -> pos:int -> special:EConstr.constr -> default:EConstr.constr -> EConstr.constr -> EConstr.types -> EConstr.constr
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