Content deleted Content added
Merge sections |
|||
Line 93:
===Proof assistant features===
Dependent types are powerful enough to encode most properties of programs, and an Idris program can prove invariants at compile-time. This makes Idris into a proof assistant.
There are two standard ways of interacting with proof assistants: by writing a series of tactic invocations ([[Coq]] style), or by interactively elaborating a proof term (Epigram/Agda style). Idris supports both modes of interaction, although the set of available tactics is not yet as useful as that of Coq.
===Code generation===
| |||