Skip to content

Instantly share code, notes, and snippets.

View _etc_nginx_sites-available
default:
server{
listen 80;
server_name impe.ga *.impe.ga *.laura-guillaume.fr;
rewrite ^(.*) https://$host$1 permanent;
}
sharelatex:
server{
@twanvl
twanvl / Sorting.agda
Created May 23, 2013
Correctness and runtime of mergesort, insertion sort and selection sort.
View Sorting.agda
module Sorting where
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Nullary