thelissimus

module Utils (module Utils) where

import Brokkr.HashTable qualified as HT

import Control.Monad
import Control.Monad.Primitive

import Data.Hashable (hashWithSalt)

instance HT.Hash ShortText where

thelissimus

module BoundedNat where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Product

record BoundedNat (min max : ℕ) : Set where
  constructor mk
  field
    val : ℕ

thelissimus

open import Function.Bundles
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality

open Equivalence

fn : {a : Set} → (a × a) ⇔ (Bool → a)
fn .to (_ , snd) false = snd
fn .to (fst , _) true  = fst

thelissimus

module MicroLens where

open import Function using (id; _∘_)
open import Data.Sum using (_⊎_) renaming (inj₁ to inl; inj₂ to inr)

record Profunctor (P : Set → Set → Set) : Set₁ where
  field
    dimap : ∀ {a' a b b'} → (a' → a) → (b → b') → P a b → P a' b'

  lmap : ∀ {a' a b} → (a' → a) → P a b → P a' b

thelissimus

\import Logic
\import Paths

\data Circle
  | base
  | loop I \with {
    | left => base
    | right => base
  }

thelissimus

import (
	"fmt"
	"strings"
)

func cypher(str string, key string) string {
	s, ix := new(strings.Builder), 0
	for _, cs := range str {
		s.WriteRune(cs + rune(key[ix%len(key)]))
		ix++

thelissimus

class Expr (F : Type → Type) where
  bool : Bool → F Bool
  not : F Bool → F Bool
  and : F Bool → F Bool → F Bool
  or : F Bool → F Bool → F Bool

  int : Int → F Int
  add : F Int → F Int → F Int
  sub : F Int → F Int → F Int

thelissimus

universe u

class Group (G : Type u) extends Add G where
  inv : G → G
  e   : G

  add_assoc     : ∀ a b c : G, (a + b) + c = a + (b + c)
  add_left_inv  : ∀ a : G, (inv a) + a = e
  add_right_inv : ∀ a : G, a + (inv a) = e
  add_left_id   : ∀ a : G, e + a = a

thelissimus

inductive Vec (α : Type u) : Nat → Type u where
| nil : Vec α 0
| cons : α → Vec α n → Vec α (n + 1)
deriving Repr

def Vec.reverse {α : Type u} {n : Nat} (xs : Vec α n) : Vec α n := loop xs nil
where
  loop {n m : Nat} : Vec α n → Vec α m → Vec α (n + m)
  | nil, acc => by rwa [Nat.zero_add]
  | @cons _ n x xs, acc => by

thelissimus

module Intro where

-- Types

data Writers : Set where
  Wilde Shelley Byron Sartre Camus : Writers

data Literature : Set where
  DorianGrey Alastor ChildeHarold LaNausée L’Étranger : Literature