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
-- Formalization of untyped lambda calculus | |
module 2013-10-23-lambda where | |
open import Level hiding (zero;suc) | |
open import Function using (_∘_;id;_⟨_⟩_) | |
open import Data.Empty | |
open import Data.Star as Star using (Star;_◅_;_◅◅_;ε;_⋆) | |
open import Relation.Binary | |
open import Relation.Binary.PropositionalEquality hiding (subst) | |
open import Data.Product as P hiding (map;zip) |
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
module Sorting where | |
-- See https://www.twanvl.nl/blog/agda/sorting | |
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax) | |
open import Data.List hiding (merge) | |
open import Data.List.Properties | |
open import Data.Nat hiding (_≟_;_≤?_) | |
open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans) | |
open import Data.Nat.Logarithm | |
open import Data.Nat.Induction |
OlderNewer