Simply Typed Lambda Calculus in Idris Syntax.idr Defines syntax and typing rules for the Simply Typed Lambda Calculus with the base type Unit. SmallStep.idr Defines small step dynamics for the language.