<div dir="ltr"><div dir="ltr"><div dir="ltr"><a href="https://lamport.azurewebsites.net/pubs/proof.pdf">https://lamport.azurewebsites.net/pubs/proof.pdf</a></div><div dir="ltr"><br></div><div>What Leslie describes can easily be done in agda. One needs to use "where" extensively to</div><div>define local lemmas. We need to improve the "C-h" command that extracts the type of the lemma from holes.</div><div>And secondly, be able to hide the proofs of the lemmas so as not to clatter the proof.</div><div><br></div><div>I would personally also use postulates inside "where" for simple things.</div><div><br></div><div>```<br></div><div>open import Data.Nat hiding (_≤_)<br>open import Relation.Binary.PropositionalEquality<br><br>f : ℕ → ℕ<br>f k = {!!} where<br>  postulate<br>    g : k + k ≡ 2 * k<br>```<br><br></div></div></div>