aztek

module RomanNumerals where

open import Data.List
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)

data Literal : Set where
  𝐼 𝑉 𝑋 𝐿 𝐶 𝐷 𝑀 : Literal

infix 4 ones_

aztek

open import Level
open import Data.List
open import Data.Sum
open import Relation.Binary

module InsertionSort {ℓ ℓ₁ ℓ₂} (totalOrder : TotalOrder ℓ ℓ₁ ℓ₂) where

open TotalOrder totalOrder renaming (Carrier to A)
open IsTotalOrder isTotalOrder renaming (trans to ≤-trans; total to _≤?_)

aztek

open import Level using (_⊔_)
open import Function
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Vec
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Core

aztek

q="eurT=fmap const pure 'q' abs;eslaF=fmap const show q gcd;xam=fmap const pure '=' odd;denifednu=ip<>di;dns=eurT<>xam;tsf=dns<>eslaF;ip=pure$!tsf;di=fmap const pure q cos;ton=dna<$>unlines;dna=putStr`fmap`yna;yna=mappend<*>reverse;main=let erehw main=main in fmap const ton denifednu main"
eurT=fmap const pure 'q' abs;eslaF=fmap const show q gcd;xam=fmap const pure '=' odd;denifednu=ip<>di;dns=eurT<>xam;tsf=dns<>eslaF;ip=pure$!tsf;di=fmap const pure q cos;ton=dna<$>unlines;dna=putStr`fmap`yna;yna=mappend<*>reverse;main=let erehw main=main in fmap const ton denifednu main

niam undefined not tsnoc pamf ni niam=niam where tel=niam;esrever>*<dneppam=any;any`pamf`rtStup=and;senilnu>$<and=not;soc q erup tsnoc pamf=id;fst!$erup=pi;False><snd=fst;max><True=snd;id><pi=undefined;ddo '=' erup tsnoc pamf=max;dcg q wohs tsnoc pamf=False;sba 'q' erup tsnoc pamf=True
"niam undefined not tsnoc pamf ni niam=niam where tel=niam;esrever>*<dneppam=any;any`pamf`rtStup=and;senilnu>$<and=not;soc q erup tsnoc pamf=id;fst!$erup=pi;F