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=9b13c3121ef87cf4d3311a8a1db43db4be7f0e5e2a702fdaff04a3b3c432cb31

sha512=81e0760ca77cb862a5bdb8927aa37faf7141c4e2484a8163dad0a3eaa21cc691acb5f72279c78588c085f53dde4bd35186346378feac0ab55ac06a679cf2e60f

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 Syntax : sig ... end

Parser-level abstract syntax.