package rocq-runtime

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

Module Indschemes.InternalSource

Sourceval do_scheme_all : user_call_scheme:bool -> declare_mind:declare_mind_function -> Libnames.qualid Constrexpr.or_by_notation -> Names.Id.t list option -> unit

Create the All predicate with its theorem all_forall.

Use the reexported function in DeclareInd instead to avoid needing to pass declare_mind.