Content deleted Content added
Tag: Reverted |
m Unexplained removal of content by Oecarl; I do recognize it is unsourced, but they also left it cut off at "when compared with", so... |
||
Line 62:
=== Metavariables ===
One of the distinctive features of Agda, when compared with other similar systems such as [[Coq]], is heavy reliance on metavariables for program construction. For example, one can write functions like this in Agda:
<syntaxhighlight lang="agda">
add : ℕ → ℕ → ℕ
add x y = ?
</syntaxhighlight>
<code>?</code> here is a metavariable. When interacting with the system in emacs mode, it will show the user expected type and allow them to refine the metavariable, i.e., to replace it with more detailed code. This feature allows incremental program construction in a way similar to tactics-based proof assistants such as Coq.
=== Proof automation ===
| |||