{{ message }}

Instantly share code, notes, and snippets.

🦄
I want to apply for a Ph.D.

# Tesla I. Zhang‮ ice1000

🦄
I want to apply for a Ph.D.
Last active Jul 13, 2021
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)}
Created May 8, 2021
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 {
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 { R visitConst(Const c, P p); R visitInfinity(P p); R visitRef(Reference r, P p); }
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
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
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

_______                   _________
___    |________________________  /
__  /| |_  ___/  _ \_  __ \  __  /

Last active May 6, 2020
Comparison among several REPLs with goal support
View repl-goal.md

# REPLs with Typed Holes

## Arend

λ> java -jar cli-1.3.0-full.jar -i
Arend REPL 1.3.0: https://arend-lang.github.io   :? for help
λ \open Nat

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
Last active Dec 15, 2019 — forked from lunalunaa/untyped-lambda.hs
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
Last active Oct 30, 2019
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