Content deleted Content added
Hairy Dude (talk | contribs) →Unicode: capitalisation Tags: Mobile edit Mobile web edit Advanced mobile edit |
Hairy Dude (talk | contribs) →Proof automation: omitting RHS Tags: Mobile edit Mobile web edit Advanced mobile edit |
||
Line 88:
</syntaxhighlight>
(The pattern <code>()</code>, called ''absurd'', matches if the type checker finds that its type is uninhabited, i.e. proves that it stands for a false proposition, typically because all possible constructors have arguments that are unavailable, i.e. they have unsatisfiable premisses. Here no value of type <code>isJust A</code> can be constructed because, in that context, no value of type <code>A</code> exists to which we could apply the constructor <code>Just</code>. The right hand side is omitted from any equation that contains absurd patterns.) Given a function <code>check-even : (n : <math>\mathbb{N}</math>) → Maybe (Even n)</code> that inputs a number and optionally returns a proof of its evenness, a tactic can then be constructed as follows:
<syntaxhighlight lang="agda">
| |||