Emit

In brief: emit keeps run. run internal is defp. Spec and evidence are omitted. Erased Π-arguments are dropped from the generated arity. A non-run fragment that somehow remains becomes raise "erased term".

From a file

iex -S mix

{:ok, src} = Muro.emit_file("examples/half_ok.muro", Foo)
IO.puts(src)

Muro.emit_file/2 parses, checks, then emits. If the book does not check, you get the error and no module.

The generated file starts with:

defmodule Foo do
  # Generated by Muro. Evidence never becomes a run.

Visibility

Tag	Elixir
run	def
run internal	defp
spec	omitted
evidence	omitted
data	omitted as a type; constructors appear only as runtime tags inside run terms

examples/internal_ok.muro: step → defp step; inc → def inc calling step.

How values look

Muro	Elixir
0	0
suc(n)	{:suc, n}
tt	:tt
0-argument ctor (nil, nothing, leaf)	atom (:nil, :nothing, :leaf)
n-argument ctor	{:ctor, args…}
left n / right t	{:left, n} / {:right, t}
run Stream	Stream.unfold/2
addi / addt / packI	Nx.add / Nx.stack / Nx.tensor

rewrite emits as its body. refl would be :refl if it ever appeared in run; it should not.

Erased arguments

Erased binders are not parameters of the Elixir function.

def length : run Π (- A : Type) → Π (xs : List A) → Nat

becomes something like def length(xs). The type argument is gone. In Muro you still write length Nat ones2 (or length A as in a recursive call). The checker sees A. Emit does not.

What emit is not

It does not type raw Elixir. It does not emit spec or evidence. It does not turn a Stream that is only evidence into Stream. It does not use Nx.Defn.

If you want a book in the test suite, parse/check/emit it from test/muro_check_test.exs. The canonical book Muro.Example.book/0 must stay in sync with examples/half_ok.muro and agda/Muro/Example.agda.

Next: Grammar.