Skip to content

Instantly share code, notes, and snippets.

View jarlg's full-sized avatar

Jarl G. Taxerås Flaten jarlg

25 followers · 15 following
View GitHub Profile
@jarlg
jarlg / time-of-build-both.log
Last active June 21, 2021 18:44
Typeclasses Transparent Commutative vs Hint Unfold
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------
3m00.69s | 528412 ko | Total Time / Peak Mem | 3m05.47s | 523492 ko || -0m04.78s || 4920 ko | -2.58% | +0.93%
----------------------------------------------------------------------------------------------------------------------------------------------------
0m24.78s | 445196 ko | Classes/implementations/natpair_integers.vo | 0m28.40s | 454156 ko || -0m03.61s || -8960 ko | -12.74% | -1.97%
0m06.87s | 399332 ko | Algebra/Groups/FreeProduct.vo | 0m08.81s | 398664 ko || -0m01.94s || 668 ko | -22.02% | +0.16%
0m04.17s | 381368 ko | Algebra/Rings/QuotientRing.vo | 0m03.09s | 378568 ko || +0m01.08s || 2800 ko | +34.95
@jarlg
jarlg / GrpCategory.v
Last active December 20, 2020 19:34
Require Import Groups.Group.
Require Import Category Categories.Structure Categories.SetCategory.
(** * The (univalent) category of groups *)
Record GroupStructure (A : hSet) := {
gp_sgop : SgOp A;
gp_unit : MonUnit A;
gp_inverse : Negate A;
gp_isgroup : IsGroup A;
@jarlg
jarlg / Parsing-complete.lhs
Last active March 8, 2018 21:03
live file (with holes) of parsing, and completed version
* Does everyone have a REPL (ghci) running?
* Literal haskell: code is on lines starting with ">".
* Run it with "ghci <file>".
* https://gist.github.com/jarlg
i) Types
Every *value* (a sequence of bits in memory) has a *type* (the
"meaning" of these bits).
@jarlg
jarlg / binaural_test_sound.py
Created October 4, 2015 09:34
small test of making audio in python
import wave
import math
import struct
samplerate = 44100
frequency1 = 220
frequency2 = 219
duration = 5
def signal():
@jarlg
jarlg / sing.html
Created October 3, 2015 15:48
js example using webaudio to analyse mic input to control an oscillator
<!DOCTYPE html>
<html>
<head></head>
<body>
<script type=text/javascript>
navigator.getUserMedia = navigator.getUserMedia
|| navigator.webkitGetUserMedia
|| navigator.mozGetUserMedia;