Revision as of 15:21, 17 March 2025 edit Hairy Dude (talk \| contribs) Extended confirmed users 91,196 edits infobox: + total Tags: Mobile edit Mobile web edit Advanced mobile edit ← Previous edit		Revision as of 15:36, 17 March 2025 edit undo Hairy Dude (talk \| contribs) Extended confirmed users 91,196 edits →Metavariables: capitalisation, grammar Tags: Mobile edit Mobile web edit Advanced mobile edit Next edit →
Line 71: add x y = ? </syntaxhighlight> <code>?</code> here is a metavariable. When interacting with the system in ~~emacs~~Emacs mode, it will show the user the 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 ===

Agda (programming language): Difference between revisions