agda

f : (A B : Set) -> Set -> Set
-- ^ C-c C-c on `f` should generate f A B x = ?

After the ring solver has been merged in (#922), we should update the README to demonstrate the new equational reasoning (instead of propositional reasoning) and the solvers.

It will be interesting to implement trees, codata, etc

Bitbucket: https://bitbucket.org/lambdamix/superspec/issue/27
Originally Reported By: Ilya Klyuchnikov
Originally Created At: 2013-08-28T09:02:42.726

Hi,

i think it would be good to update the agda-mode/README.md here in the agda mode in order to specify which commands are shared with Emacs, which commands are only available here in Agda mode, and which commands are only on Emacs and pending integration with Atom.

I could edit the changes if we discuss them in this thread.

agda

Here are 135 public repositories matching this topic...

agda / agda

HoTT / HoTT-Agda

agda / agda-stdlib

EgbertRijke / HoTT-Intro

martinescardo / HoTT-UF-Agda-Lecture-Notes

copumpkin / categories

awesomo4000 / awesome-provable

ilya-klyuchnikov / ttlite

martinescardo / TypeTopology

scott-fleischman / agda-from-nothing

alhassy / next-700-module-systems

banacorn / agda-mode

algebraic-graphs / agda

gallais / generic-syntax

gallais / agdarsec

fredefox / cat

alhassy / gentle-intro-to-reflection

jespercockx / ataca

scott-fleischman / greek-grammar

wenkokke / AutoInAgda

oisdk / agda-ring-solver

gallais / agda-sizedIO

L-TChen / MtacAR

alhassy / AgdaCheatSheet

ice1000 / ConsHoTT

wenkokke / msla2014

jpvillaisaza / cain

gallais / agda-presburger

agda / agda-pkg

mr-ohman / logrel-mltt

Improve this page

Add this topic to your repo