wenkokke

#!/bin/bash
set -eo pipefail

# 1. Build GHC with JavaScript backend
# https://gitlab.haskell.org/ghc/ghc/-/wikis/javascript-backend/building

# 2. Get Agda source
git clone --depth=1 git@github.com:agda/agda.git agda
cd agda

wenkokke

from contextlib import contextmanager
from curses.ascii import isalpha
from dataclasses import dataclass
from pathlib import Path
import ast
import re
from typing import Any, Optional, Sequence, Set


@dataclass

wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

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

wenkokke

cheatsheet.tex
*.aux
*.fls
*.log
*.synctex.gz
*.fdb_latexmk
*.lot

wenkokke

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes   #-}

module Lib where

data Nat = Z
         | S Nat

-- There's something really wonky going on with closed type families: if both

wenkokke

%if False
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% linear.fmt
%
% Format -> as a period when part of a lambda abstraction,
% as a lolli when used as part of a linear function arrow,
% and as an arrow otherwise.
%
% Wen Kokke, February 2021, version 1.0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

wenkokke

{-(- by Wen Kokke, borrowing heavily from CS410-17 lecture 1 by Conor McBride -)-}

module lecture1 where

module sum-and-product-types where

{--------------------------------------------------------------------------------}
-- so Coq and Agda are kinda the same, yet very different

-- * it's said Coq looks like ML and Agda looks like Haskell

wenkokke

#! /usr/bin/env python3

from csv      import reader, writer
from datetime import datetime, timedelta
from optparse import OptionParser
from sys      import stderr


# parse command line options
parser = OptionParser()

wenkokke

Keybase proof

I hereby claim:

• I am wenkokke on github.
• I am wen (https://keybase.io/wen) on keybase.
• I have a public key ASDGrBG6vQXq3xYQEocI-PSLS6yli9zR3hLMpoYidQQz2go

To claim this, I am signing this object:

wenkokke

{-# LANGUAGE RecordWildCards #-}

import Data.Char (toUpper)
import Data.List (intersperse)
import Text.Printf (printf)

-- |The definition of a non-deterministic finite-state automata.
--  Note: this definition assumes that all epsilon transitions
--  have been removed from the NFA.
data NFA s c = NFA