Skip to content

Instantly share code, notes, and snippets.

View ice1000's full-sized avatar
♾️
Generalizing something

Tesla Zhang‮ ice1000

♾️
Generalizing something
3.8k followers · 716 following
View GitHub Profile
@fgoinai
fgoinai / EWhen.kt
Created May 31, 2017 13:53
fun <T: Comparable<T>> eWhen(target: T, tester: Tester<T>.() -> Unit) {
val test = Tester(target)
test.tester()
test.funFiltered?.invoke() ?: return
}
class Tester<T: Comparable<T>>(val it: T) {
var funFiltered: (() -> Unit)? = null
infix fun Boolean.then(block: () -> Unit) {
@AndrasKovacs
AndrasKovacs / UnivPoly.hs
Last active June 14, 2021 07:23
simple universe polymorphism
{-# language LambdaCase, Strict, BangPatterns, ViewPatterns, OverloadedStrings #-}
{-# options_ghc -Wincomplete-patterns #-}
module UnivPoly where
import Data.Foldable
import Data.Maybe
import Data.String
import Debug.Trace
@philard
philard / SuperBreakpoint.java
Last active September 18, 2021 08:37
String className = (this != null) ? this.getClass().getSimpleName() : "";
int wavFilesCount = new java.io.File("sounds").listFiles().length;
int clipIndex = (className.hashCode() & 0x7FFFFFFF) % wavFilesCount;
javax.sound.sampled.Clip clip = javax.sound.sampled.AudioSystem.getClip();
java.io.File wavFile = new java.io.File("sounds" + java.io.File.separator + "sound" + clipIndex + ".wav");
javax.sound.sampled.AudioInputStream audio = javax.sound.sampled.AudioSystem.getAudioInputStream(wavFile);
clip.open(audio);
clip.start();
@fgoinai
fgoinai / FnChain.py
Last active July 26, 2022 02:49
Just for chain invocation of function
from functools import partial, reduce
from itertools import chain
from typing import Callable, Any, Sequence, Optional, Mapping
class FnChain:
"""
FnChain(obj).map(...).filter(...).reduce(...)...
API LIST:
@ncfavier
ncfavier / Niltok-coh.agda
Last active August 4, 2022 09:31
[WIP] Equivalence between the "coherentified" version of @ice1000's Niltok type and the booleans
open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import Data.Bool
data Niltok : Type where
t : Niltok
nicht : Niltok → Niltok
mod2 : (n : Niltok) → n ≡ nicht (nicht n)
coh : (n : Niltok) → ap nicht (mod2 n) ≡ mod2 (nicht n)
@lambdageek
lambdageek / Array-In-InferRule.md
Last active February 27, 2023 17:33
LaTeX array within inferrule from mathpartir

Sometimes I want to put an array inside of a mathpartir inferrule.

The straightforward thing doesn't work:

\begin{equation*}
\inferrule{Conclusion}{
  Premiss 1 \and
  \begin{array}{ll}
 1 &amp; 2 \\ % note, this is where the problem happens
@matchy233
matchy233 / Microsoft.PowerShell_profile.ps1
Created April 22, 2023 12:52
Remove duplicated downloaded files
Function Remove-DupDownloads {
param (
[string]$SearchPath = ".",
[switch]$Recurse = $false
)
$FilePattern = '.*\([1-9][0-9]*\).*'
$GCIParams = @{
'Path' = $SearchPath
'File' = $true
@bobatkey
bobatkey / cont-cwf.agda
Last active June 16, 2023 21:23
Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted
{-# OPTIONS --rewriting #-}
module cont-cwf where
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq
@jespercockx
jespercockx / PropRezz.agda
Created February 22, 2018 19:13
The great resurrection of Prop
{-
======================================
=== THE GREAT RESURRECTION OF PROP ===
======================================
Bringing back the impredicative sort Prop of definitionally proof-irrelevant propositions to Agda.
To check this file, get the prop-rezz branch of Agda at https://github.com/jespercockx/agda/tree/prop-rezz.
This file is a short demo meant to show what you currently can (and can't) do with Prop.
@Trebor-Huang
Trebor-Huang / Quotient.agda
Last active October 10, 2023 16:03
Quotient types in MLTT imply excluded middle
open import Agda.Builtin.Equality
-- Some familiar results about equality
UIP : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q
UIP x y refl refl = refl
coerce : {A : Set} (B : A → Set)
→ {x y : A} → x ≡ y
→ B x → B y