Folder
Homonyms
neural/eidos/specs/surface
surface the user-facing language for eidos. surface syntax is what users write; the elaborator translates it to kernel terms (see terms). the elaborator is untrusted โ bugs in it produce terms the kernel rejects, not false theorems. grammar application is left-associative: `f a b c` parses asโฆ