Extended version of Agda in which we have added an ATP-pragma

License: Other

Language: Haskell

Extended version of Agda

Build Status


We have extended the development version of Agda in order to handle a new built-in ATP-pragma.

This version of Agda is used for reasoning about functional programs by combining interactive and automatic proofs (see


You can download our extended version of Agda using Git with the following command:

$ git clone

This will create a directory called eagda. Installing our extended version is similar to the installation of Agda (see for more information). In our setup, we run the first time the following commands:

$ cd eagda
$ make install-bin
$ agda-mode setup

To test the installation of the extended version of Agda, type-check a module which uses the new built-in ATP-pragma, for example

module Test where

data _∨_ (A B : Set) : Set where
  inj₁ : A  A ∨ B
  inj₂ : B  A ∨ B

  A B    : Set
  ∨-comm : A ∨ B  B ∨ A
{-# ATP prove ∨-comm #-}

Project Statistics

Sourcerank 5
Repository Size 82.3 MB
Stars 0
Forks 0
Watchers 1
Open issues disabled
Dependencies 2
Contributors 77
Tags 30
Last updated
Last pushed

Top Contributors See all

Andreas Abel Ulf Norell Andrés Sicard-Ramírez Nils Anders Danielsson Jesper Cockx Philipp Hausmann Andrea Vezzosi G. Allais Francesco Mazzoli Fredrik Nordvall Forsberg Dominique Devriese Víctor López Juan Péter Diviánszky Paolo G. Giarrusso Nicolas Pouillard Stevan Andjelkovic Daniel Gustafsson James Chapman Guillaume Brunerie Jean-Philippe Bernardy

Recent Tags See all

apia-1.0.0 April 01, 2016 February 13, 2016 December 18, 2015 December 13, 2015 October 14, 2015 May 25, 2015 May 19, 2015 November 26, 2014 November 13, 2014 July 29, 2014
2_4_0 June 05, 2014
2_3_2_2 September 27, 2013
2_3_2_1 June 04, 2013
2_3_2 November 12, 2012
2_3_0 November 23, 2011

Something wrong with this page? Make a suggestion

Last synced: 2018-02-04 13:35:29 UTC

Login to resync this repository