Content deleted Content added
m fix title, add website name |
→Code generation: removed vague statement |
||
Line 97:
===Code generation===
Because Idris contains a proof assistant, Idris programs can be written to pass proofs around. If treated naïvely, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms
By default, Idris generates native code through [[C (programming language)|C]]. The other officially supported backend generates [[JavaScript]].
|