Termination check (structural induction)

owo-lang / minitt-rs

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust

Apache License 2.0

113 stars 3 forks source link

Termination check (structural induction) #9

Open ice1000 opened 5 years ago

zaoqi commented 4 years ago

Has this feature been implemented?

ice1000 commented 4 years ago

Neither minitt-rs nor voile-rs has termination check. If you wanna have a try, I'll recommend working on Voile because of the term structure. In Voile, the Neutral::App AST element is in spine-normal form, which is friendly for arguments traversals.