Gaupy

default:
server{
        listen 80;
        server_name impe.ga *.impe.ga *.laura-guillaume.fr;
        rewrite ^(.*) https://$host$1 permanent;
}


sharelatex:
server{

twanvl

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