[Agda] ANN: coq-like agda-mode support for databases of lemmas

[Nils Anders Danielsson]

On 2011-05-28 01:09, Wojciech Jedynak wrote:
>   This makes me want to ask a general question: is there any support in
>   agda-mode for writing proofs that heavily use the ≡-Reasoning
>   notations (like \==\<  and \qed) by hand? Or, say, for automatically
>   indenting proofs written in this style?

You can use C-u M-x align-regexp, and use a regexp like "\(\s-*\) [≡∎]".

-- 
/NAD