SekiT

defmodule ApplicativeMaybe do
  @type t(a) :: {:just, a} | :nothing

  @spec pure(val :: a) :: t(a) when a: var
  def pure(val), do: {:just, val}
  
  @spec fmap(f :: (a -> b), ma :: t(a)) :: t(b) when a: var, b: var
  def fmap(f, {:just, val}), do: {:just, f.(val)}
  def fmap(_, :nothing    ), do: :nothing
  

SekiT

// Promise that resolves with n, after n seconds
const wait = n => new Promise(resolve => setTimeout(() => resolve(n), n * 1000))

// Promise that rejects with n, after n seconds
const failAfter = n => new Promise((_, reject) => setTimeout(() => reject(n), n * 1000))

Promise.all([wait(1), wait(2), wait(3)]).then(console.log)
// => Resolves with [1, 2, 3] after 3 seconds
Promise.all([wait(1), failAfter(2), wait(3)]).catch(console.log)
// => Rejects with 2 after 2 seconds

SekiT

plus_assoc : (a : Nat) -> (b : Nat) -> (c : Nat) -> plus a (plus b c) = plus (plus a b) c
plus_assoc Z     b c = Refl
plus_assoc (S a) b c = rewrite plus_assoc a b c in Refl

plus_unit : (a : Nat) -> a = plus a Z
plus_unit Z     = Refl
plus_unit (S a) = rewrite plus_unit a in Refl

plus_commutes_S : (a : Nat) -> (b : Nat) -> S (plus a b) = plus a (S b)
plus_commutes_S Z     b = Refl

SekiT

double_negate : a -> (a -> Void) -> Void
double_negate a not_a = not_a a

double_negate_rev : Dec a -> ((a -> Void) -> Void) -> a
double_negate_rev (Yes proof_a) _ = proof_a
double_negate_rev (No contra_a) f = absurd (f contra_a)

counter_position : (a -> b) -> (b -> Void) -> (a -> Void)
counter_position f g = g . f

SekiT

data FizzDataType : Type where
  FizzData : FizzDataType

data BuzzDataType : Type where
  BuzzData : BuzzDataType

data FizzBuzzDataType : Type where
  FizzBuzzData : FizzBuzzDataType

data NatDataType : (n : Nat) -> Type where

SekiT

module Term

%default total

data Term : Type where
  Zero   : Term
  True   : Term
  False  : Term
  Succ   : Term -> Term
  Pred   : Term -> Term

SekiT

module NamelessLambda

%default total
%access public export

data Term: Type where
  Var    : Nat -> Term
  Lambda : Term -> Term
  Apply  : Term -> Term -> Term

SekiT

module Main

import Data.Vect

infixr 5 .+.

data Schema
  = SString
  | SChar
  | SInt

SekiT

module ZZ

import Data.Sign

%default total
%access public export

data Diff : Nat -> Nat -> Type where
  LTByS : (d : Nat) -> Diff n (n + S d)
  GTByS : (d : Nat) -> Diff (n + S d) n

SekiT

import ZZ

%default total

integralDomainN : Not (m = Z) -> Not (n = Z) -> Not (m * n = Z)
integralDomainN mNotZ nNotZ mnEqZ {m = Z} = mNotZ Refl
integralDomainN mNotZ nNotZ mnEqZ {n = Z} = nNotZ Refl
integralDomainN mNotZ nNotZ mnEqZ {m = S a} {n = S b} = uninhabited mnEqZ

infixl 9 |>