[Agda] How to write proofs by Leslie Lamport : Hierarchical structures

[Apostolis Xekoukoulotakis]

https://lamport.azurewebsites.net/pubs/proof.pdf

What Leslie describes can easily be done in agda. One needs to use "where"
extensively to
define local lemmas. We need to improve the "C-h" command that extracts the
type of the lemma from holes.
And secondly, be able to hide the proofs of the lemmas so as not to clatter
the proof.

I would personally also use postulates inside "where" for simple things.

```
open import Data.Nat hiding (_≤_)
open import Relation.Binary.PropositionalEquality

f : ℕ → ℕ
f k = {!!} where
  postulate
    g : k + k ≡ 2 * k
```
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190131/1c55f370/attachment.html>