package lambdapi

  1. Overview
  2. Docs
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type

Configuration for tactics based on first-order logic.

type config = {
  1. symb_P : Core.Term.sym;
    (*

    Encoding of propositions.

    *)
  2. symb_T : Core.Term.sym;
    (*

    Encoding of types.

    *)
  3. symb_or : Core.Term.sym;
    (*

    Disjunction(∨) symbol.

    *)
  4. symb_and : Core.Term.sym;
    (*

    Conjunction(∧) symbol.

    *)
  5. symb_imp : Core.Term.sym;
    (*

    Implication(⇒) symbol.

    *)
  6. symb_bot : Core.Term.sym;
    (*

    Bot(⊥) symbol.

    *)
  7. symb_top : Core.Term.sym;
    (*

    Top(⊤) symbol.

    *)
  8. symb_not : Core.Term.sym;
    (*

    Not(¬) symbol.

    *)
  9. symb_ex : Core.Term.sym;
    (*

    Exists(∃) symbol.

    *)
  10. symb_all : Core.Term.sym;
    (*

    Forall(∀) symbol.

    *)
}

Builtin configuration for propositional logic.

val get_config : Core.Sig_state.t -> Common.Pos.popt -> config

get_config ss pos build the configuration using ss.