justarandomgeek

do local foo="bar"
--[[ The line above must start with "do local" to be recognized as a decompressed blueprint.
     Adjust rombase to control the first memory address the rom is generated for.
     Adjust addrsignal below to control memory address signal. Requires a compatible machine, and address signal cannot be stored.
     data is array of parameter lists for constant combinators.
     
     strings are converted to serialized frames and appended to data. No terminators are added.
     pixeldata is converted and added after strings.
  ]]

WillDignazio

#include <stdlib.h>
#include <fcntl.h>
#include <stdio.h>
#include <errno.h>

/*
 * There may not be a userspace definition yet since
 * at the time of this gist, 3.11 is only in rc2.
 */
#ifndef O_TMPFILE

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