proof(idris2): tighten Ephapax.Affine.Emit to %default total

[hyperpolymath]

Summary

Ninth and final file in the ephapax %default partial → totality-tightening campaign. After this lands together with the rest, no %default partial remains anywhere in ephapax/idris2/src/Ephapax/.

The file is a one-line wrapper:

emitModule: Module -> String
emitModule = encode

Its totality is exactly Ephapax.IR.Decode.encode's. On the chain's exit state (with PR #96 merged), encode is covering — the show . toSExpr pipeline inherits covering from Decode's recursive encode/decode functions (justified in #96's body).

Mark emitModulecovering to match. Flip file default %default partial → %default total. The covering modifier on the one defined function is the entirety of the "escape" footprint — explicit, narrow, justified.

No assert_total / believe_me.

Verification

$ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Affine/Emit.idr
1/4: Building Ephapax.IR.SExpr
2/4: Building Ephapax.IR.AST
3/4: Building Ephapax.IR.Decode
4/4: Building Ephapax.Affine.Emit

Refs — the full campaign

• #124 (proof-debt audit epic)
• #134 (ephapax totality sub-issue)

#	File	PR	Annotation outcome
1	IR/SExpr.idr	#89	%default total, fueled mutual parser
2	Parse/Stream.idr	#90	%default total, fueled remaining/build
3	Parse/Util.idr	#91	%default total, fueled many + sepBy.sepTail
4	Parse/Lexer.idr	#93	%default total, fueled lex.go (57 call sites)
5	IR/AST.idr	#94	%default total + 6 retained covering (showPrec/(/=) loop)
6	IR/Decode.idr	#96	%default total + 7 covering (map/traverse SCT limit)
7	Affine/Typecheck.idr	#97	%default total + pre-existing baseline-rot layout fix
8	Parse/Parser.idr	#99	%default covering (LL(k) Stream-recursion, ~30 fns, large refactor deferred)
9	Affine/Emit.idr	this	%default total + 1 covering (inherits from Decode.encode)

Test plan

• idris2 --check Ephapax/Affine/Emit.idr builds green under %default total
• CI green
• No assert_* / believe_me; only covering on emitModule (matches dependency)

🤖 Generated with Claude Code