This gist is my attempt to list all projects providing proof automation for Agda.
When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:
_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3
| ; Emulating cps call using LLVM Coroutines | |
| ; RUN: opt coro-cps.ll -O2 -enable-coroutines -S | |
| define void @f(i32 %arg) { | |
| entry: | |
| %bar.ret.addr = alloca i32 | |
| %id = call token @llvm.coro.id(i32 0, i8* null, i8* null, i8* null) | |
| %size = call i32 @llvm.coro.size.i32() | |
| %alloc = call i8* @malloc(i32 %size) | |
| %hdl = call noalias i8* @llvm.coro.begin(token %id, i8* %alloc) |
| This is my short-ish tutorial on how to implement closures in | |
| a simple functional language: Foo. | |
| First, some boilerplate. | |
| > {-# LANGUAGE DeriveFunctor, TypeFamilies #-} | |
| > import Control.Applicative | |
| > import Control.Monad.Gen | |
| > import Control.Monad.Writer | |
| > import Data.Functor.Foldable |