package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.kernel/Cooking/index.html

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 -> UVars.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