package lambdapi

  1. Overview
  2. Docs

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

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.

OCaml

Innovation. Community. Security.