Skip to content

Instantly share code, notes, and snippets.


Carter Tazio Schonwald cartazio

View GitHub Profile
cartazio / finitary.agda
Created Jan 4, 2022 — forked from atennapel/finitary.agda
Finitary non-indexed datatype signatures
View finitary.agda
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ty : Set where
U : Ty
Pi : (A : Set) -> (A -> Ty) -> Ty
PiInd : Ty -> Ty
cartazio / howto grep
Last active Sep 7, 2021
how to grep all of hackage!
View howto grep

first decide where to place your local copy of stuff


how to get the most recent version of everything

cabal list --simple | awk '{print ($1)}' | uniq | time xargs -P20 -n1 cabal get

then use grep/ ripgrep or whatever to find where code exists/is used/ is defined

then look at the matches

View examples-fromListN.hs
$ rg -e fromListN -t haskell ./
139: let termCounts = V.fromListN (M.size nodeItems)
174: let termCounts = V.fromListN (M.size nodeItems)
171: let termCounts = V.fromListN (M.size nodeItems)
View babyCalculusEqations.hs
d/dx (x ^ a) == d/dx (a -> x )
we never consider a ^ x === x -> a ()
log_x(\nu Y -> T) == \mu Z -> log_X T , where Z == log_X Y
(translation: every time we see log_X Y , in T, replace taht with Z )
View Sadd.hs
module Main where
import Data.Word
import Data.Int
import Foreign.Ptr
import Foreign.C.Types
main = c_MD5Final `seq` print "yay"
cartazio / StructExample.hs
Created Jun 6, 2019
hacky unfinished scribblings about how to do fancy struct instances
View StructExample.hs
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ExplicitForAll#-}
module Main where
import Data.Struct
--import Data.Struct.TH
--import qualified Data.Coerce as Crc
import Data.Coerce (coerce)
View chordCorrect.als
/* ========================================================================
Pamela Zave, August 2016.
Copyright AT&T Labs, Inc., 2016, 2018.
======================================================================== */
open util/ordering[Time] as trace
open util/ordering[Node] as ring
cartazio / packagesize.txt
Last active Feb 19, 2019
rounded up to the nearest megabyte, generated with du -hm -d1 ./ | sort -rn
View packagesize.txt
143 .//sugarhaskell-0.1
122 .//morfette-0.4.7
53 .//http2-1.6.4
40 .//cjk-
39 .//qt-
37 .//uhc-light-
37 .//cld2-
33 .//texmath-0.11.2
33 .//happstack-yui-7373.5.3
32 .//scholdoc-texmath-
cartazio / fixYoMath.r
Last active Feb 11, 2019
NAN NAN you cant get the undefined float value man
View fixYoMath.r
install("inline")# not needed after the first time
nanBoom <- cfunction(c(dummy="ANY"),body="
fenv_t fenv;
unsigned int new_excepts = FE_DIVBYZERO | FE_INVALID ;
fenv.__mxcsr &= ~(new_excepts << 7);
return dummy;
",includes="#include <fenv.h>",language="C")
cartazio / simplemat.c
Created Jan 29, 2019
old matrix mat code
View simplemat.c
// #include <emmintrin.h>
#include <immintrin.h>
// #if defined (__SSE4_2__) || defined (__SSE4_1__)
// for some reason i can't get anything newer than sse4.2 work with both gcc-clang and clang
// #include <smmintrin.h>
// #endif
#include <memory.h>