Instantly share code, notes, and snippets.

# Liang-Ting Chen L-TChen

Last active April 14, 2022 06:09
Normalization by evaluation for System T with the normalization proof and the confluence proof
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -} open import Data.Empty using (⊥) open import Data.Unit using (⊤; tt) open import Data.Nat using (ℕ; zero; suc) open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) infix 3 _-→_ _-↛_
Created August 19, 2020 08:46
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 open import Data.Nat open import Data.Empty hiding (⊥-elim) open import Relation.Nullary open import Relation.Binary.PropositionalEquality hiding ([_]) infix 3 _⊢_ _=β_ infixr 7 _→̇_
Last active August 20, 2020 15:42

# Intrinsically-typed de Bruijn representation of simply typed lambda calculus

```open import Data.Nat
open import Data.Empty
hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality```
Created July 27, 2020 11:47
Go to definitions in Agda mode combined with Evil mode in Emacs

Evil mode overwrites the mouse-2 event which is used by Agda to go to the definition of clicked identifier. To restore the desired behavioru, just add the following line after enabling Evil `(require 'evil)`

``````(define-key evil-normal-state-map [mouse-2] 'agda2-goto-definition-mouse)
``````
Last active March 22, 2019 20:15
Some experiments with --prop and instance arguments
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {-# OPTIONS --safe --prop --overlapping-instances #-} module Playground where open import Data.Nat open import Data.List open import Data.Bool open import Data.Empty open import Data.Unit
Created February 26, 2019 14:43
Lambda Terms which are Sized, Scoped, Indexed by (potentially) free variables
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 open import Relation.Binary open import Relation.Binary.PropositionalEquality hiding ([_]) module Term.Base (Atom : Set)(_≟A_ : Decidable {A = Atom} (_≡_)) where open import Relation.Nullary public open import Data.Nat renaming (_≟_ to _≟ℕ_) open import Data.Fin renaming (_≟_ to _≟F_) hiding (_+_; compare) open import Data.Product hiding (map) open import Data.List
Last active January 22, 2019 22:48
An imperative implementation of Union-Find algorithm in Haskell
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {-# LANGUAGE BangPatterns #-} module Union where import Data.Ix import Data.Array import Data.Array.ST import Control.Monad import Control.Monad.ST
Last active January 18, 2019 19:14
Purely Functional Deque
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {-# LANGUAGE ViewPatterns, PatternSynonyms #-} module Deque where import Text.Read import Data.Bifunctor import Prelude hiding (length, init, tail, last, head) import qualified Prelude as P data Deque a =
Last active January 3, 2019 09:09
The derivation of Quickselect from Quicksort, see my blog post https://xcycl.wordpress.com/2019/01/02/fromquicksorttoquickselect/
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {-# LANGUAGE TypeApplications #-} import Test.QuickCheck import Data.List (sort) selectOrigin k = (!! k) . sort select :: (Ord a) => Int -> [a] -> a select k (x:xs) = case compare k n of LT -> select k ys EQ -> x
Last active June 30, 2023 13:42
Pattern matching for Vector using PatternSynonyms in Haskell
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE PatternSynonyms #-} import Data.Vector as V pattern Empty :: Vector a pattern Empty <- (V.null -> True) where Empty = V.empty uncons :: Vector a -> Maybe (a, Vector a) uncons Empty = Nothing