package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Proof.StepSource

An inference step is composed of a set of premises, a rule, a status (theorem/trivial/equisatisfiable…), and is used to deduce new result using these premises and metadata.

A single step can be used to deduce several results.

Sourcetype t = step
Sourceval kind : t -> kind
Sourceval parents : t -> parent list
Sourceval infos : t -> infos
Sourceval compare : t -> t -> int
Sourceval hash : t -> int
Sourceval equal : t -> t -> bool
Sourceval src : t -> source option
Sourceval trivial : t
Sourceval by_def : ID.t -> t
Sourceval define : ID.t -> source -> parent list -> t
Sourceval define_internal : ID.t -> parent list -> t
Sourceval lemma : source -> t
Sourceval intro : source -> role -> t
Sourceval assert_ : source -> t
Sourceval assert' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
Sourceval goal : source -> t
Sourceval goal' : ?loc:Loc.t -> file:string -> name:string -> unit -> t
Sourceval inference : ?infos:infos -> ?tags:tag list -> rule:rule -> parent list -> t
Sourceval simp : ?infos:infos -> ?tags:tag list -> rule:rule -> parent list -> t
Sourceval esa : ?infos:infos -> rule:rule -> parent list -> t
Sourceval to_attrs : t -> UntypedAST.attrs
Sourceval is_trivial : t -> bool
Sourceval is_by_def : t -> bool
Sourceval is_assert : t -> bool

Proof: the statement was asserted in some file

Sourceval is_goal : t -> bool

The statement comes from the negation of a goal in some file

Sourceval rule : t -> rule option

Rule name for Esa/Simplification/Inference steps

Sourceval distance_to_goal : t -> int option

distance_to_conjecture p returns None if p has no ancestor that is a conjecture (including p itself). It returns Some d if d is the distance, in the proof graph, to the closest conjecture ancestor of p

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