package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a

doc/lambdapi.parsing/Parsing/SearchQuerySyntax/index.html

Module Parsing.SearchQuerySyntaxSource

Sourcetype side =
  1. | Lhs
  2. | Rhs
Sourcetype inside =
  1. | Exact
  2. | Inside
Sourcetype 'inside where =
  1. | Spine of 'inside
  2. | Conclusion of 'inside
  3. | Hypothesis of 'inside
Sourcetype constr =
  1. | QType of inside option where option
  2. | QXhs of inside option * side option
Sourcetype base_query =
  1. | QName of string
  2. | QSearch of Syntax.p_term * bool * constr option
Sourcetype op =
  1. | Intersect
  2. | Union
Sourcetype filter =
  1. | Path of string
Sourcetype query =
  1. | QBase of base_query
  2. | QOpp of query * op * query
  3. | QFilter of query * filter
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