package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module CookingSource

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

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

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

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
Sourceval lift_private_poly_univs : cooking_info -> Univ.ContextSet.t -> Univ.ContextSet.t
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