Skip to content

Instantly share code, notes, and snippets.

View petercommand's full-sized avatar
:octocat:
Github!

Ptrcmd petercommand

:octocat:
Github!
38 followers · 44 following
View GitHub Profile
@petercommand
petercommand / ModTest.agda
Created November 8, 2019 14:47
module ModTest where
module A (f : Set) where
data T : Set where
t : T
module B (f : Set) where
open A f
test : T → T
test k = {!!}
@petercommand
petercommand / sqrt2.agda
Last active October 19, 2019 15:27
Square 2 is irrational
{- agda 2.6.0.1, stdlib v1.1 -}
open import Data.Nat renaming (_*_ to _*ℕ_; _+_ to _+ℕ_; suc to sucℕ)
open import Data.Nat.Properties
open import Data.Nat.Coprimality renaming (sym to coprime-sym)
open import Data.Nat.Divisibility
open import Data.Nat.GCD
open import Data.Integer renaming (_*_ to _*ℤ_)
open import Data.Product
open import Data.Empty
open import Relation.Nullary
@petercommand
petercommand / t-n.agda
Last active July 25, 2017 08:32
open import Data.Fin hiding (_<_; _≤_; _+_)
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Data.Nat.Properties.Simple
ℕ- : (a b : ℕ) → a ≥ b → ℕ
ℕ- a .0 z≤n = a
ℕ- (suc m) (suc n) (s≤s p) = ℕ- m n p
@petercommand
petercommand / w.agda
Created September 15, 2016 11:43
data W (S : Set) (P : S -> Set) : Set where
sup : (s : S) (f : P s -> W S P) -> W S P
data ⊥ : Set where
record ⊤ : Set where
data Bool : Set where
tt : Bool
ff : Bool
@petercommand
petercommand / test.agda
Created July 19, 2016 13:46
open import HoTT
open import lib.Univalence
bool-not : Bool -> Bool
bool-not true = false
bool-not false = true
bool-not-id : ∀ b -> bool-not (bool-not b) == b
bool-not-id true = idp
@petercommand
petercommand / parse.hs
Last active May 4, 2016 11:13
module Main where
import Data.Map (Map)
import qualified Data.Map as M
import System.IO
import System.Environment
import Language.Haskell.Exts.Annotated
import Control.DeepSeq
import Control.Monad
import Debug.Trace
@petercommand
petercommand / gist:ac9a497c091c81a26436
Last active August 29, 2015 14:14
simple lisp calculator
#include <stdlib.h>
#include <stdio.h>
#include <memory.h>
enum {
OPERATOR,
NUMERAL,
SEPARATOR
};
enum {
@petercommand
petercommand / gist:c44943d8e88f9f6cb0d9
Created August 25, 2014 15:11
#include <stdlib.h>
#include <string.h>
#include <stdio.h>
#include <time.h>
#include <sys/time.h>
#include <math.h>
/*please note that this program treat type char as signed, different platform may produce different result */
typedef struct{
char str[12];
@petercommand
petercommand / gist:5e920eea459092675eeb
Created August 13, 2014 16:18
euler:~/LilyTerm $ ./configure
Checking GTK+2 ......................... [OK]
Checking VTE ........................... [OK]
Checking Native Language Support ....... [NO]
=================================================
PREFIX = /usr/local
ETCDIR = $(PREFIX)/etc/xdg
DEBUG = N
@petercommand
petercommand / gist:7b20df3700689f142361
Created August 13, 2014 15:45
euler:/ $ HOMEBREW_MAKE_JOBS=1 brew install -v pygobject 2>&1
==> Downloading http://ftp.gnome.org/pub/GNOME/sources/pygobject/2.28/pygobject-2.28.6.tar.bz2
Already downloaded: /Library/Caches/Homebrew/pygobject-2.28.6.tar.bz2
==> Verifying pygobject-2.28.6.tar.bz2 checksum
tar xf /Library/Caches/Homebrew/pygobject-2.28.6.tar.bz2
==> Downloading http://git.gnome.org/browse/pygobject/patch/gio/gio-types.defs?id=42d01f060c5d764baa881d13c103d68897163a49
Already downloaded: /Library/Caches/Homebrew/pygobject--patch-6976bbad5212ae775e6715405e0e70e592356db2.defs
==> Verifying pygobject--patch-6976bbad5212ae775e6715405e0e70e592356db2.defs checksum
==> Patching
/usr/bin/patch -g 0 -f -d /private/tmp/pygobject-9TOy/pygobject-2.28.6 -p1 -i /private/tmp/pygobject--patch-BIsh/gio-types.defs