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 · 713 following
View GitHub Profile
@ice1000
ice1000 / MultiplyCircle.agda
Created April 19, 2021 05:06
Credit to Lambda Duck, I'm just posting it here for sharing convenience
{-# 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 February 5, 2021 16:46
Implementing a lean example in 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 / EgbertPropTrunc.agda
Created January 15, 2021 15:59
Solution to some propositional truncation problems :)
-- twitter thread: https://twitter.com/EgbertRijke/status/1349865209591173120
{-# OPTIONS --cubical #-}
open import Cubical.HITs.PropositionalTruncation using (∥_∥; ∣_∣; squash; rec)
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Function using (_∘_; idfun)
open import Cubical.Data.Sigma using (_×_; fst; snd)
import Cubical.Data.Empty as ⊥ using (elim)
@ice1000
ice1000 / arend-ascii-big-text.md
Created April 28, 2020 20:51
A collection of ASCII art for "Arend"

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 01:14
Comparison among several REPLs with goal support
@ice1000
ice1000 / Bools.ard
Created April 24, 2020 20:04
Transport over Bool.not
\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
@ice1000
ice1000 / untyped-lambda.hs
Last active December 15, 2019 05:07 — forked from lunalunaa/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
@ice1000
ice1000 / infnat.agda
Last active October 30, 2019 00:14
{-# 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
@ice1000
ice1000 / linked_list_incomplete.hpp
Created August 30, 2018 20:54
Incomplete linked list
#ifdef _MSC_VER
#pragma once
#endif
#ifndef LIST_HPP
#define LIST_HPP
#include <cstddef>
#include <iterator>
#include <initializer_list>
@ice1000
ice1000 / Printf.agda
Created August 7, 2018 16:02
Type safe printf
--- http://ice1000.org/gist/safe-printf-agda/
module Printf where
open import Data.List using (List; _∷_; [])
open import Data.Char renaming (Char to ℂ)
open import Data.Nat using (ℕ; _+_)
open import Data.Nat.Show renaming (show to showℕ)
open import Data.Empty
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (yes; no)