asr/eagda


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

License: Other

Language: Haskell


Extended version of Agda

Build Status

Description

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 README.md).

Installation

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

$ git clone https://github.com/asr/eagda.git

This will create a directory called eagda. Installing our extended version is similar to the installation of Agda (see README.md 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

postulate
  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
Created
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
2.5.0.20160213 February 13, 2016
2.4.2.5 December 18, 2015
2.4.2.4.20151210 December 13, 2015
2.4.2.4 October 14, 2015
2.4.2.3 May 25, 2015
2.4.2.2.20150518 May 19, 2015
2.4.2.2 November 26, 2014
2.4.2.1 November 13, 2014
2.4.0.2 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