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=04fac3b56d1855795d7d2d2442bc650183bcd71f676c3ea77f37240e33769ce9

sha512=37f7bec3bc48632379ca9fb3eb562a0c0387e54afbdd10fb842b8da70c6dad529bb98c14b9d7cddf44a1d5aa61bba86338d310e6a7b420e95b2996b4fbafc95c

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.

Sourceval simpl : (Core.Term.term -> Core.Term.term) -> goal -> goal

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

Sourceval pp : goal Lplib.Base.pp

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

Sourceval pp_hyps : goal Lplib.Base.pp

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