anka-213’s gists

anka-213 / HangarbackWalker.agda

Created August 21, 2024 14:29

	{-# OPTIONS --postfix-projections #-}
	open import Relation.Binary.PropositionalEquality
	open import Function
	open import Data.Nat
	open import Data.Nat.Properties
	open import Data.Fin using (Fin ; #_)
	open import Data.Unit.Base hiding (_≤_)
	open import Data.Empty
	open import Data.Bool hiding (_≤_)
	open import Data.Product

anka-213 / day3.hs

Created December 3, 2023 19:39

Haskell solution of Advent of Code 2023 day 3

	{-# LANGUAGE TypeApplications #-}
	import Data.Char
	import Data.Bifunctor (second)
	import Data.Function
	import Data.List

	main = interact $ solution . lines

	map3 f (a,b,c) = (f a, f b, f c)

anka-213 / xkcd_2712.js

Created December 20, 2022 13:15

Turn wayfinder into a labeled minimap in xkcd 2712

	Comic.wayfinderFarDistance = 80000
	Comic.wayfinderSpread = 300

	Comic.wayfinderEls.forEach((x,i) => (x.innerText = i, x.style.color = 'red'))

	M = (v, min, max) => Math.min(Math.max(v,min),max)
	window.origUpdateWayfinder = window.origUpdateWayfinder \|\| Comic.updateWayfinder
	Comic.updateWayfinder = Function("return function " + origUpdateWayfinder.toString().replace("+10", "+this.wayfinderSpread"))()

anka-213 / CheckStrictness.hs

Last active January 6, 2024 10:03

A type class for statically checking if data is fully strict

	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE UndecidableInstances #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FlexibleContexts #-}

	module CheckStrictness where
	import GHC.Generics

anka-213 / Exercises6-my-general.lagda.md

Created August 4, 2022 13:13

A solution of the generalization of Exercise 6 from the HoTTest summer school, with a Wedge of k circles instead of a bowtie. Based on my previous generalization for Bowtie.

    {-# OPTIONS --rewriting --without-K --allow-unsolved-metas #-}

open import new-prelude

open import Lecture6-notes
open import Lecture5-notes

anka-213 / Exercises6-my.lagda.md

Created August 4, 2022 13:12

A slightly DRYer solution of Exercise 6 form the HoTTest summer school, where the common part between loop1 and loop2 has been combined

    {-# OPTIONS --rewriting --without-K --allow-unsolved-metas #-}

open import new-prelude

open import Lecture6-notes
open import Lecture5-notes

anka-213 / GenericToTree.hs

Last active November 29, 2020 12:58

A module for converting any data type with a Generic instance into a pretty tree

	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE DefaultSignatures #-}
	{-# LANGUAGE TypeApplications #-}
	{-# LANGUAGE AllowAmbiguousTypes #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE DeriveGeneric #-}
	{-# LANGUAGE ScopedTypeVariables #-}

anka-213 / CoinChange.hs

Created October 24, 2020 23:50


	coinSet = [1, 2, 5, 10, 20, 50, 100, 150, 200, 300]

	-- When no coins are available, there is one way to get 0, no ways to get any other number
	coins0 = 1:repeat 0

	-- Given the result for previous coins, produce a list of possibilities for this coin type
	coinsN coin preCoins = go
	where
	-- We can either get the value by using other coins or from an earlier value in this list

anka-213 / AlgebraicData.hs

Created June 26, 2020 19:49

All finite data structures of the same size (cardinality) can be converted between each other and to/from a finite (peano) number

	{-

	Algebraic data is called such because the ways to define a type
	correspond to the basic algebra operations for numbers:

	An empty type Void corresponds to 0
	The unit type () corresponds to 1
	A sum type Either x y corresponds to x + y
	A product type (x, y) corresponds to x * y

anka-213 / gist:2b8882b25b82038b976764019228c874

Created June 18, 2020 21:00

Contents of /nix/store/j6w8a63v99z8hhyay1di6k8f7chxmzqq-source

	/nix/store/j6w8a63v99z8hhyay1di6k8f7chxmzqq-source
	├── neuron.cabal
	├── src
	│ ├── app
	│ │ ├── Data
	│ │ │ └── Structured
	│ │ │ └── Breadcrumb.hs
	│ │ ├── Main.hs
	│ │ └── Neuron
	│ │ ├── CLI

Andreas Källberg anka-213