package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TemplateAritySource

Sourcetype template_binder = {
  1. bind_sort : Sorts.t;
  2. default : Sorts.t;
}

NB: the types and rel_contexts may mention previous args eg "sigT : forall A, (A -> Type) -> Type" is "TemplateArg (, u, TemplateArg (_:Rel 1, v, IndType (_, , Type@max(u,v))))" note the "Rel 1"

Sourceval get_template_arity : Environ.env -> Names.inductive -> ctoropt:int option -> template_arity