package rocq-runtime

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

Module UGraph.InternalSource

Sourceval add_template_qvars : Sorts.QVar.Set.t -> t -> t

Makes the qvars treated as above prop. Do not use outside kernel inductive typechecking.

Sourceval is_above_prop : t -> Sorts.QVar.t -> bool