package rocq-runtime

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

Module AllScheme.Warning_scheme_allSource

Sourcetype cache
Sourcetype t
Sourceval empty_cache : unit -> cache
Sourceval warn : t -> cache -> unit

Warning for looking up the all predicate and its theorem. If this warning is alredy in the cache do nothing, oterwise warn and add it to the cache