Modules
ShotTo provides a decidable instance of the βη-long-normal Computability
Path Order (NCPO-LNF) of Niederhauser and Middeldorp (NCPO goes
Beta-Eta-Long Normal Form, 2025) for terms of Church's simple type theory
as represented by the shot_ds library.
Implementation of NCPO-LNF (the βη-long-normal Computability Path Order).
Parameters that define a concrete instance of NCPO-LNF.
Admissible type order ≻_T and related predicates used by NCPO-LNF.