package orthologic-coq

  1. Overview
  2. Docs
A plugin to add orthologic-based tactics to Coq

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

  1. S
    Simon Guilloud
  2. C
    Clément Pit-Claudel

Maintainers

  1. S
    Simon Guilloud

Sources

orthologic-coq-0.9.1.tbz
sha256=60a9eeb27b6ad0a6fadb4127f5a7fdc194133dc55fa627e5eaedbee58a58651e
sha512=bab767857cecbb1529e599785f2485e62171a55b7ec34483976a9a15e8223167c52a2977f88752e64f17fd1b4e6fde682b608bd046b2a7867da2eca10844cf57

doc/orthologic-coq.plugin/OLCoq/Ol/index.html

Module OLCoq.OlSource

Sourceval total_formula : int ref
Sourceval total_polar : int ref
Sourceval total_normal : int ref
Sourcetype formula =
  1. | Variable of {
    1. id : int;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
  2. | Neg of {
    1. child : formula;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
  3. | Or of {
    1. children : formula list;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
  4. | And of {
    1. children : formula list;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
  5. | Literal of {
    1. b : bool;
    2. unique_key : int;
    3. mutable polar_formula : polar_formula option;
    }
Sourceand polar_formula =
  1. | PolarVariable of {
    1. id : int;
    2. polarity : bool;
    3. unique_key : int;
    4. mutable inverse : polar_formula option;
    5. mutable normal_form : normal_formula option;
    }
  2. | PolarAnd of {
    1. children : polar_formula list;
    2. polarity : bool;
    3. unique_key : int;
    4. mutable inverse : polar_formula option;
    5. mutable normal_form : normal_formula option;
    }
  3. | PolarLiteral of {
    1. b : bool;
    2. unique_key : int;
    3. mutable inverse : polar_formula option;
    4. mutable normal_form : normal_formula option;
    }
Sourceand normal_formula =
  1. | NormalVariable of {
    1. id : int;
    2. polarity : bool;
    3. unique_key : int;
    4. mutable inverse : normal_formula option;
    5. mutable formulaP : formula option;
    6. mutable formulaN : formula option;
    7. lt_cache : (int, bool) Hashtbl.t;
    }
  2. | NormalAnd of {
    1. children : normal_formula list;
    2. polarity : bool;
    3. unique_key : int;
    4. mutable inverse : normal_formula option;
    5. mutable formulaP : formula option;
    6. mutable formulaN : formula option;
    7. lt_cache : (int, bool) Hashtbl.t;
    }
  3. | NormalLiteral of {
    1. b : bool;
    2. unique_key : int;
    3. mutable inverse : normal_formula option;
    4. mutable formulaP : formula option;
    5. mutable formulaN : formula option;
    6. lt_cache : (int, bool) Hashtbl.t;
    }
Sourceval new_variable : int -> formula
Sourceval new_neg : formula -> formula
Sourceval new_or : formula list -> formula
Sourceval new_and : formula list -> formula
Sourceval new_literal : bool -> formula
Sourceval new_p_variable : int -> bool -> polar_formula
Sourceval new_p_and : polar_formula list -> bool -> polar_formula
Sourceval new_p_literal : bool -> polar_formula
Sourceval new_n_variable : int -> bool -> normal_formula
Sourceval new_n_and : normal_formula list -> bool -> normal_formula
Sourceval new_n_literal : bool -> normal_formula
Sourceval get_key : formula -> int
Sourceval get_polar_formula : formula -> polar_formula option
Sourceval set_polar_formula : formula -> polar_formula option -> unit
Sourceval get_p_normal_form : polar_formula -> normal_formula option
Sourceval set_p_normal_form : polar_formula -> normal_formula option -> unit
Sourceval size : formula -> int
Sourceval get_p_key : polar_formula -> int
Sourceval get_p_inverse_option : polar_formula -> polar_formula option
Sourceval set_p_inverse_option : polar_formula -> polar_formula option -> unit
Sourceval get_n_key : normal_formula -> int
Sourceval get_n_inverse_option : normal_formula -> normal_formula option
Sourceval set_n_inverse_option : normal_formula -> normal_formula option -> unit
Sourceval get_formulaP : normal_formula -> formula option
Sourceval set_formulaP : normal_formula -> formula option -> unit
Sourceval get_formulaN : normal_formula -> formula option
Sourceval set_formulaN : normal_formula -> formula option -> unit
Sourceval get_lt_cache : normal_formula -> (int, bool) Hashtbl.t
Sourceval lt_cached : normal_formula -> normal_formula -> bool option
Sourceval set_lt_cached : normal_formula -> normal_formula -> bool -> unit
Sourceval formula_to_string : formula -> string
Sourceval polar_formula_to_string : polar_formula -> string
Sourceval normal_formula_to_string : normal_formula -> string
Sourceval get_polar_inverse : polar_formula -> polar_formula
Sourceval polarize : formula -> bool -> polar_formula
Sourceval get_normal_inverse : normal_formula -> normal_formula
Sourceval to_formula_nnf : normal_formula -> bool -> formula
Sourceval to_formula : normal_formula -> formula
Sourceval lattices_leq : normal_formula -> normal_formula -> bool
Sourceval simplify : normal_formula list -> bool -> normal_formula
Sourceval check_for_contradiction : normal_formula -> bool
Sourceval polar_to_normal_form : polar_formula -> normal_formula
Sourceval reduced_form : formula -> formula
Sourceval show_ol : unit -> unit
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