package lambdapi

  1. Overview
  2. Docs

Module Handle.FolSource

Configuration for tactics based on first-order logic.

Sourcetype config = {
  1. symb_Prop : Core.Term.sym;
    (*

    Type of propositions.

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

    Encoding of propositions.

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

    Type of sets.

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

    Encoding of types.

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

    Disjunction(∨) symbol.

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

    Conjunction(∧) symbol.

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

    Implication(⇒) symbol.

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

    Equivalence(⇔) symbol.

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

    Bot(⊥) symbol.

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

    Top(⊤) symbol.

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

    Not(¬) symbol.

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

    Exists(∃) symbol.

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

    Forall(∀) symbol.

    *)
}

Builtin configuration for propositional logic.

get_config ss pos build the configuration using ss.