package lambdapi

You can search for identifiers within the package.

in-package search v0.2.0

Proof assistant for the λΠ-calculus modulo rewriting

Install

dune-project

Dependency

sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed

sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8

Sourcetype t = goal

Sourceval ctxt : goal -> Core.Term.ctxt

ctxt g returns the typing context of the goal g.

Sourceval env : goal -> Core.Env.t

env g returns the scoping environment of the goal g.

Sourceval of_meta : Core.Term.meta -> goal

of_meta m creates a goal from the meta m.

val simpl : 
  (Core.Term.ctxt -> Core.Term.term -> Core.Term.term) ->
  goal ->
  goal

simpl f g simplifies the goal g with the function f.

Sourceval bindlib_ctxt : goal -> Bindlib.ctxt

bindlib_ctxt g computes a Bindlib context from a goal.

Sourceval pp : goal Lplib.Base.pp

pp ppf g prints on ppf the goal g without its hypotheses.

Sourceval hyps : goal Lplib.Base.pp

hyps ppf g prints on ppf the hypotheses of the goal g.