Revision as of 21:01, 13 November 2014 edit Jec (talk \| contribs) Extended confirmed users 1,173 edits Stub →Proof assistant features ← Previous edit		Revision as of 21:08, 13 November 2014 edit undo Jec (talk \| contribs) Extended confirmed users 1,173 edits Stub →Code generation Next edit →
Line 99: ===Code generation=== Because Idris contains a proof assistant, Idris programs can be written to pass proof around. If treated naively, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms<ref>https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis</ref>, with promising results<ref>http://ziman.functor.sk/erasure-bm/</ref>. By default, Idris generates native code by going through C. Other backends are available for generating Javascript and Java. ==References==

Idris (programming language): Difference between revisions