Skip to content

Instantly share code, notes, and snippets.

View kana-sama's full-sized avatar
🌚

kana kana-sama

🌚
View GitHub Profile
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecursiveDo #-}
import Control.Concurrent
import Control.Concurrent.STM
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLabels #-}
@kana-sama
kana-sama / these-n.hs
Last active September 16, 2021 22:57
These
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
import Data.Aeson (FromJSON (..), decode, withObject, (.:))
import Data.Proxy (Proxy (..))
import data.string.basic
import system.io
def unlines := string.intercalate "\n"
def unwords := string.intercalate " "
def range : ∀n, list (fin n)
| 0 := []
| (n+1) := (range n).map (λ⟨a, h⟩, ⟨a, h.step⟩) ++ [⟨n, nat.less_than_or_equal.refl⟩]
@kana-sama
kana-sama / q.lean
Created July 22, 2021 19:51
Thinking with Types: TicTacToe
import data.string.basic
import system.io
def unlines := string.intercalate "\n"
def unwords := string.intercalate " "
abbreviation ix := fin 3
namespace ix
def op : ix → ix
| ⟨0, _⟩ := 2
{-# LANGUAGE ImplicitParams #-}
import qualified Data.Char as Char
import Data.Foldable (traverse_)
import Data.IORef (IORef, modifyIORef', newIORef, readIORef)
import Data.Word (Word8)
data Instruction
= MoveR
| MoveL
name: erlchat-test
dependencies:
- base >= 4.12 && < 5
- servant
- servant-server
- warp
- stm
- mtl
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}