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.tool/Tool/Sr/index.html

Module `Tool.Sr`Source

Checking that a rule preserves typing (subject reduction property).

Sourceval check_rule : Parsing.Scope.pre_rule Common.Pos.loc -> Core.Term.rule

check_rule r checks whether the pre-rule r is well-typed in signature state ss and then construct the corresponding rule. Note that Fatal is raised in case of error.