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=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be

sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c

Sourcemodule DkBasic : sig ... end

Part of the Dedukti source file kernel/basic.ml.

Sourcemodule DkLexer : sig ... end

Dedukti source file parsing/lexer.mll.

Sourcemodule DkParser : sig ... end

Sourcemodule DkRule : sig ... end

Sourcemodule DkTokens : sig ... end

Dedukti source file parsing/tokens.ml.

Sourcemodule LpLexer : sig ... end

Sourcemodule LpParser : sig ... end

Sourcemodule Package : sig ... end

Find and read lambdapi.pkg files.

Sourcemodule Parser : sig ... end

Parsing functions for Lambdapi.

Sourcemodule Pratt : sig ... end

Parsing of infix operators using the Pratter library.

Sourcemodule Pretty : sig ... end

Pretty-printing the parser-level AST.

Sourcemodule Scope : sig ... end

Scoping. Convert parsed terms in core terms by finding out which identifiers are bound variables or function symbol declared in open modules.

Sourcemodule SearchQuerySyntax : sig ... end

Sourcemodule Syntax : sig ... end

Parser-level abstract syntax.