Notices by pounce (pounce@nyan.network)

@nik @pie @shmibs in short it’s supposed to look like haskell but also every tiny bit of it at every stage of code elaboration and parsing and generating is overridable at runtime which is awesome also all unicode is supported

in dependent type theory you usually have lots of things that have the form “x:T + proof x is something” which is a “subset type” of T Fin n is a finite subset of the naturals of numbers less that n so the type is literally “number + proof number is less than n” that’s what the angly brackets are, and the things past the commas in the brackets are my proofs that the numbers are truly less than what they say they are

it’s like zero cost abstractions on steroids (this all compiles to very efficient C, where allOf 10 would just compile to an array of 0-9)