package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.0.tar.gz

sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

doc/coq-core.kernel/Cooking/index.html

Module `Cooking`Source

Data needed to abstract over the section variables and section universes

The instantiation to apply to generalized declarations so that they behave as if not generalized: this is the a1..an instance to apply to a declaration c in the following transformation: a1:T1..an:Tn, C:U(a1..an) ⊢ v(a1..an,C):V(a1..an,C) ~~> C:Πx1..xn.U(x1..xn), a1:T1..an:Tn ⊢ v(a1..an,Ca1..an):V(a1..an,Ca1..an) note that the data looks close to the one for substitution above (because the substitution are represented by their domain) but here, local definitions of the context have been dropped

Sourcetype abstr_inst_info

Sourcetype 'a entry_map = 'a Names.Cmap.t * 'a Names.Mindmap.t

Sourcetype expand_info = abstr_inst_info entry_map

The collection of instantiations to be done on generalized declarations + the generalization to be done on a specific judgment: a1:T1,a2:T2,C:U(a1) ⊢ v(a1,a2,C):V(a1,a2,C) ~~> c:Πx.U(x) ⊢ λx1x2.(v(a1,a2,cx1)[a1,a2:=x1,x2]):Πx1x2.(V(a1,a2,ca1)[a1,a2:=x1,x2]) so, a cooking_info is the map c ↦ x1..xn, the context x:T,y:U to generalize, and the substitution x,y

Sourcetype cooking_info

Sourceval empty_cooking_info : cooking_info

Nothing to abstract

Source

val make_cooking_info : 
  recursive:Names.MutInd.t option ->
  expand_info ->
  Constr.named_context ->
  Univ.UContext.t ->
  cooking_info * abstr_inst_info

Abstract a context assumed to be de-Bruijn free for terms and universes

Sourceval names_info : cooking_info -> Names.Id.Set.t

Sourceval universe_context_of_cooking_info : cooking_info -> Univ.AbstractContext.t

Sourceval instance_of_cooking_info : cooking_info -> Constr.t array

Sourcetype cooking_cache

Sourceval create_cache : cooking_info -> cooking_cache

Sourceval instance_of_cooking_cache : cooking_cache -> Constr.t array

Sourceval rel_context_of_cooking_cache : cooking_cache -> Constr.rel_context

Sourceval abstract_as_type : cooking_cache -> Constr.types -> Constr.types

Sourceval abstract_as_body : cooking_cache -> Constr.constr -> Constr.constr

Sourceval abstract_as_sort : cooking_cache -> Sorts.t -> Sorts.t

Source

val lift_mono_univs : 
  cooking_info ->
  Univ.ContextSet.t ->
  cooking_info * Univ.ContextSet.t

Source

val lift_poly_univs : 
  cooking_info ->
  Univ.AbstractContext.t ->
  cooking_info * int * Univ.AbstractContext.t

The int is how many universes got discharged, ie size of returned context - size of input context.

Sourceval lift_private_mono_univs : cooking_info -> 'a -> 'a

Source

val lift_private_poly_univs : 
  cooking_info ->
  Univ.ContextSet.t ->
  Univ.ContextSet.t

Source

val discharge_proj_repr : 
  cooking_info ->
  Names.Projection.Repr.t ->
  Names.Projection.Repr.t

On This Page

Data needed to abstract over the section variables and section universes

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Cooking/index.html

Module CookingSource

Data needed to abstract over the section variables and section universes

Module `Cooking`Source