Viewing profile — omegafixedpoint

Seconding Debruijn indices. See here: https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53... The alpha renaming algorithm does not run under scopes, only lambdas.

Yeah it really is a mess. One of the most egregious things I noticed was that variables under lambdas are STRINGS: https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53... T…

Had some edits I made halfway through, so I was a bit hasty. It is dependently-typed in that the only valid codomain of a \Pi type is the identity type, Sigma, or another Pi. You c…

A few notes, because this is obviously vibe coded, and does not work in many ways. 1. Yon's documentation mentions "Homotopy type theory:" > the runnable HoTT fragment is refl/pair…