[Agda] Holes 0.1.0

[Nils Anders Danielsson]

On 2017-01-27 15:00, Bradley Hardy wrote:
> First, I’ll mention that explicitly marking where we want to rewrite
> was a design choice for this library. The idea is that it potentially
> makes things clearer to the reader while not actually being much of a
> burden to the writer (at least compared to writing out `cong (\h ->
> …)` everywhere…). And it saves having to do any kind of proof search,
> so type-checking is quick!

I have a similar tactic:

   http://www.cse.chalmers.se/~nad/listings/equality/Tactic.By.html

However, this tactic does not allow the user to mark where the argument
lemma should be applied, and can be rather slow: it tries to use
reflexivity or the argument (applied to metas, possibly with symmetry
applied), and if this fails, then it checks if the heads of the two
expressions are equal, and in this case it continues recursively
(roughly speaking).

An advantage of this approach is that you can sometimes get away with
writing "by lemma", even though this lemma is used multiple times, with
different arguments, to prove an equality. However, as I wrote above, it
can be rather slow. Furthermore it can fail if the two sides do not have
syntactically equal "contexts".

-- 
/NAD