raichoo

module Main where

main :: IO ()
main = putStrLn "this\n\
                \is  \n\
                \a   \n\
                \test"

raichoo

class GimmeThis {
  a : number;

  constructor(a : number) {
    this.a = a;
  }

  // When I pass this method as a function, "this"
  // will be bound to the "this" at the call site.
  // Should have used a function literal here to

raichoo

module Main

%lib Node "readline"

data ReadLine = MkReadLine Ptr

readlineClose : ReadLine -> IO ()
readlineClose (MkReadLine rl) =
  mkForeign (FFun "%0.close()" [FPtr] FUnit) rl

raichoo

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}

raichoo

{-# OPTIONS --copatterns #-}
module Test where

open import Data.Nat
open import Data.Bool
open import Data.Vec hiding (map; head; tail; take)

record Functor (F : Set → Set) : Set₁ where
  field
    map : ∀ {A B} → (A → B) → F A → F B

raichoo

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Test where

newtype ENumber    = ENumber Int
newtype EBoolean   = EBoolean Bool

data EIf c t f  = EIf c t f
data EAdd l r   = EAdd r l

raichoo

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Web.Scotty
import Data.Text.Lazy hiding (filter)
import Control.Concurrent.STM
import Control.Monad.IO.Class
import Data.List (nub)

storeTODO :: Text -> TVar [Text] -> STM [Text]

raichoo

module WTypes where

import Level

data W(S : Set)(T : S → Set) : Set where
  _◁_ : (s : S) → (f : T s → W S T) → W S T

data ⊤ : Set where
  ⟨⟩ : ⊤

raichoo

module Main

data FormatTy = FormatInt FormatTy
              | FormatChar Char FormatTy
              | FormatEnd

total
interpTy : FormatTy -> Type
interpTy (FormatInt ty)    = Int -> interpTy ty
interpTy (FormatChar x ty) = interpTy ty

raichoo

%default total

cyclicAdd : Fin 4 -> Fin 4 -> Fin 4
cyclicAdd x y = head $ drop (finToNat x + finToNat y) fins
  where
    fins : Stream (Fin 4)
    fins = 0 :: 1 :: 2 :: 3 :: fins