I hereby claim:
- I am favonia on github.
- I am favonia (https://keybase.io/favonia) on keybase.
- I have a public key ASCGlfRtcmUII_C0EtGiRXoRtwG21ECCnZ504VtZajdUJwo
To claim this, I am signing this object:
#include <stdio.h> | |
#include <ft2build.h> | |
#include FT_FREETYPE_H | |
#include <freetype/ftsnames.h> | |
int main (int argc, const char *argv[]) { | |
if (argc != 2) return -1; | |
FT_Library lib; | |
memset(&lib, 0, sizeof lib); |
import Control.Monad | |
import Data.List | |
import Data.Ord | |
type Cell a = (Integer,[a]) | |
type Row a = [Cell a] | |
lcs :: Eq a => [a] -> [a] -> [a] | |
lcs [] _ = [] | |
lcs _ [] = [] |
-- Released under CC0. | |
import System.IO | |
import Control.Applicative | |
type Code = [Cmd] | |
data Cmd = L | R | I | D | P | G | W Code deriving Show | |
data CodeZipper = CZ Code [(Code,Code)] deriving Show | |
data DataZipper = DZ [Int] Int [Int] deriving Show |
{-# OPTIONS --type-in-type #-} | |
-- Burali-Forti's paradox in MLTT-ish without W-types | |
-- I was following Coquand's paper "An Analysis of Girard's Paradox" | |
-- and Hurkens's paper "A Simplification of Girard's Paradox". | |
-- Code is released under CC0. | |
-- Σ-types | |
record Σ (A : Set) (B : A → Set) : Set where |
-- released under CC0 by favonia | |
import System.Environment | |
quotes :: [String -> String] | |
quotes = map q $ cycle [("「", "」"), ("『", "』")] | |
where q (l,r) str = l ++ str ++ r | |
warn :: (String -> String) -> String -> String | |
warn q str = concat ["分享", q str, "難判定有無違法,盡量不要分享", q str, ",以免觸法。"] |
I hereby claim:
To claim this, I am signing this object:
import bool | |
import s1 | |
import isotoequiv | |
let not/equiv : equiv bool bool = | |
iso→equiv _ _ (not, (not, (not∘not/id/pt, not∘not/id/pt))) | |
let not/path : path^1 type bool bool = | |
ua _ _ not/equiv |
import path | |
let cube/2loop | |
(A : type) (a : A) | |
(sq : [i j] A [∂[i j] → a]) | |
: [i j k] A [ | |
| ∂[i] → sq j k | |
| ∂[j] → sq i k | |
| ∂[k] → sq i j | |
] |
import Data.Char | |
import Data.List | |
import Control.Applicative | |
up :: String -> String | |
up = map toUpper | |
convertWord :: String -> String | |
convertWord = intercalate "\\ls " . map pure . up |
AGDA_FILES=$(wildcard *.agda) | |
TEX_FILES=${AGDA_FILES:.agda=.tex} | |
PDF_FILES=${AGDA_FILES:.agda=.pdf} | |
MONO_FONT=DejaVu Sans Mono # FreeMono is another choice | |
PYGMENTS_STYLE=tango | |
GRADED_XOPP_FILES=$(wildcard *-graded.xopp) | |
GRADED_PDF_FILES=${GRADED_XOPP_FILES:.xopp=.pdf} | |
.PHONY: all |