package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val occurrences_map : ('a list -> 'b list) -> 'a Locus.occurrences_gen -> 'b Locus.occurrences_gen
val convert_occs : Locus.occurrences -> bool * int list
val is_selected : int -> Locus.occurrences -> bool
val is_all_occurrences : 'a Locus.occurrences_gen -> bool
val allHypsAndConcl : 'a Locus.clause_expr
val allHyps : 'a Locus.clause_expr
val onConcl : 'a Locus.clause_expr
val nowhere : 'a Locus.clause_expr
val onHyp : 'a -> 'a Locus.clause_expr
val is_nowhere : 'a Locus.clause_expr -> bool
val simple_clause_of : (unit -> Names.Id.t list) -> Locus.clause -> Locus.simple_clause
val concrete_clause_of : (unit -> Names.Id.t list) -> Locus.clause -> Locus.concrete_clause
val occurrences_of_goal : Locus.clause -> Locus.occurrences
val in_every_hyp : Locus.clause -> bool
val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool
val clause_with_generic_context_selection : 'a Locus.clause_expr -> bool
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct