package lambdapi

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

Module Proof.GoalSource

Sourcetype t = goal

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.

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

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

Sourceval pp : Format.formatter -> goal -> unit

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

Sourceval pp_no_hyp : Format.formatter -> goal -> unit

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

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