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

[Nils Anders Danielsson]

On 2011-05-26 23:42, Wojciech Jedynak wrote:
> Databases do not have to be declared. All you need to do is to insert
> a comment of the form:
> {- BASE name-of-database lemma_1 lemma_2 ... lemma_n -}

Wouldn't it be nicer to use ordinary Agda definitions to define
databases? In fact, this is already possible:

module Test where

   open import Data.Nat
   open import Data.Product
   open import Relation.Binary.PropositionalEquality
   open ≡-Reasoning

   postulate
     right-identity : ∀ n → n + 0 ≡ n
     move-suc       : ∀ m n → suc (m + n) ≡ m + suc n

   db = right-identity ,′ move-suc

   comm : ∀ m n → m + n ≡ n + m
   comm m n = {!-c db!}

--
/NAD