Skip to content

Instantly share code, notes, and snippets.

Avatar
🦄
I want to apply for a Ph.D.

Tesla I. Zhang‮ ice1000

🦄
I want to apply for a Ph.D.
View GitHub Profile
View quiver-macros.tex
\newcommand{\lrbracket}[1]{\llbracket #1 \rrbracket}
\newcommand{\Tm}[2]{\text{Tm}(#1, #2)}
\newcommand{\FF}{\mathcal F}
\newcommand{\CC}{\mathcal C}
\newcommand{\EE}{\mathcal E}
\newcommand{\lrangle}[1]{\langle#1\rangle}
\newcommand{\Prop}{\text{Prop}}
\newcommand{\El}[1]{\text{El}(#1)}
\newcommand{\eqlz}[2]{\mathrm{eq}(#1,#2)}
\newcommand{\Eqlz}[2]{\mathrm{Eq}(#1,#2)}
View ProblemEquationNoVisitor.java
import java.util.List;
import java.util.Map;
public class Main {
interface Level {
}
record Const(int constant) implements Level {
}
record Infinity() implements Level {
}
record Reference(Var ref, int lift) implements Level {
@ice1000
ice1000 / ProblemEquation.java
Created May 8, 2021
Random graph theory problem
View ProblemEquation.java
import java.util.List;
import java.util.Map;
public class Main {
interface Level {
// Pattern matcher
interface Visitor<P, R> {
R visitConst(Const c, P p);
R visitInfinity(P p);
R visitRef(Reference r, P p);
}
@ice1000
ice1000 / MultiplyCircle.agda
Created Apr 19, 2021
Credit to Lambda Duck, I'm just posting it here for sharing convenience
View MultiplyCircle.agda
{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.HITs.S1
SInt : Type₀
SInt = base ≡ base
@ice1000
ice1000 / MHLLeanTIZAgdaCompetition.agda
Created Feb 5, 2021
Implementing a lean example in Agda
View MHLLeanTIZAgdaCompetition.agda
{- Lean 4
open list
#eval filter (= 4) [1, 2, 4]
-}
open import Data.Nat renaming (ℕ to Nat; _≟_ to decEqNat)
open import Data.List using (List; []; _∷_)
open import Data.Bool using (true; false)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
@ice1000
ice1000 / arend-ascii-big-text.md
Created Apr 28, 2020
A collection of ASCII art for "Arend"
View arend-ascii-big-text.md

A collection of ASCII art for "Arend"

... that doesn't look crazy to me.

Speed

_______                   _________
___    |________________________  /
__  /| |_  ___/  _ \_  __ \  __  / 
@ice1000
ice1000 / repl-goal.md
Last active May 6, 2020
Comparison among several REPLs with goal support
View repl-goal.md
@ice1000
ice1000 / Bools.ard
Created Apr 24, 2020
Transport over Bool.not
View Bools.ard
\data Bool1 | tt1 | ff1 \where {
\func to2 (b : Bool1) : Bool2
| tt1 => Bool2.tt2
| ff1 => Bool2.ff2
\lemma lemma (b : Bool1) : Bool2.to1 (to2 b) = b
| tt1 => idp
| ff1 => idp
}
\data Bool2 | tt2 | ff2 \where {
\func to1 (b : Bool2) : Bool1
View untyped-lambda.hs
{-# LANGUAGE LambdaCase #-}
data Term
= TmVar Integer
| TmAbs String Term
| TmApp Term Term
deriving (Show, Eq)
termShift :: Integer -> Term -> Term
termShift d = walk 0
View infnat.agda
{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything
open import Cubical.Data.Maybe
open import Cubical.Data.Nat
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
data ω : Type₀ where