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

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

#! /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

{-(- 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

%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

{-# 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

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

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

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

#!/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 [email protected]:agda/agda.git agda
cd agda