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

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

Authors

D

Deducteam

Maintainers

D

dedukti-dev@inria.fr

Sources

lambdapi-2.1.0.tbz

sha256=04fac3b56d1855795d7d2d2442bc650183bcd71f676c3ea77f37240e33769ce9

sha512=37f7bec3bc48632379ca9fb3eb562a0c0387e54afbdd10fb842b8da70c6dad529bb98c14b9d7cddf44a1d5aa61bba86338d310e6a7b420e95b2996b4fbafc95c

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

Module `Parsing.Pratt`Source

Parsing of infix operators using the Pratter library.

The interface for the Pratter library can be seen at

see https://forge.tedomum.net/koizel/pratter
.

Sourcemodule Pratt : sig ... end

include module type of struct include Pratt end

Sourceval parse : Core.Sig_state.t -> Core.Env.t -> Syntax.p_term -> Syntax.p_term

parse ss env t Pratt parses term t, unsugaring infix operators and prefix operators using signature state ss and environment env to determine which term is an operator, and to build new terms. Note that it doesn't recurse into abstractions or implications and alike.