omegafixedpoint

6 ms·

1. 1.▲
   by omegafixedpoint 3mo ago

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

   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... This is extremely dangerous a
3. 3.▲
   by omegafixedpoint 3mo ago

   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 can substitute variables, so Id can contain terms, but an arb
4. 4.▲
   by omegafixedpoint 3mo ago

   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/fst/snd These are b