Tesla Zhang‮

@re-xyr Agda asks you to write latex

@re-xyr Imagine we use markdown, where aya code interpolated into some markup text. Then we codegen to latex by compiling aya to latex code blocks and markup text to latex...

@re-xyr It'll be treated as plain text

> Agda supports lagda.tex and lagda.md and lagda.rst etc. I think we just have to translate the parts in the code blocks to properly rendered code? This is actually a...

Maybe we need `match` expressions for this 🤔

Problem: surely we can type-check a pattern in an expression, _but_ what to do afterward? Do we create another core language expression for pattern lambdas? What about using `match` expressions?

有生之年系列

We need to implement aya-prover/aya-prover-proto#150 (which, I guess, is related to aya-prover/aya-prover-proto#128) first

... and built-in definitions.

I mean pragmas that make definitions interact with built-in features