Kazark

module Bijection

%default total
%access public export

infixr 5 <=>

record (<=>) a p where
  constructor Biject
  ap : a -> p

Kazark

#include <limits.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

typedef struct MaybeULong {
  const unsigned long nothing;
  const unsigned long x;
} MaybeULong;

Kazark

export PROMPT_COMMAND="__posh_git_ps1 '${debian_chroot:+($debian_chroot)}\[\033[01;32m\]\u@\h\[\033[01;34m\] \w' '\[\033[34m\]\$\[\033[00m\] '"

Kazark

module AndOr

%default total
%access private

TData : Type -> Type -> Nat -> Type
TData a _ Z = a
TData a b (S Z) = (a, b)
TData _ b (S (S Z)) = b
TData _ _ _ = Void

Kazark

module Guard

%default total
%access public export

data Guarded : (a -> Bool) -> a -> Type where
  Guard : (pred : a -> Bool) -> (subject : a) -> (prf : pred subject = True)
        -> Guarded pred subject

data GuardedIsBogus : Type where

Kazark

module Id where

open import Relation.Binary.PropositionalEquality.Core
open import Function

data Id : Set → Set where
  Itself : ∀{A} → A → Id A

fmap : ∀{A B} → (A → B) → Id A → Id B
fmap f (Itself x) = Itself (f x)

Kazark

module Data.ThisOrThese where

open import Data.List.Base
open import Data.List.NonEmpty
open import Relation.Binary.PropositionalEquality.Core
open import Function

-- Apparently this is called ValidatedNel in Cats.
data ThisOrThese : Set -> Set -> Set where
  These : ∀ {A B} -> List⁺ A -> ThisOrThese A B

Kazark

module EnvDemo

open System
open System.IO

[<Struct>]
type Nothing =
    private
    | Nothing

Kazark

class Nothing : Exception {}

public static class Maybe {
  public static void Nothing() => throw new Nothing();
  public static void Guard(bool cond) { if (!cond) Nothing(); }
  public static void GuardNot(bool cond) { if (cond) Nothing(); }
}

public static class TryParse {
  public static UInt32 UInt32(string x) {

Kazark

/// Example encoding of the shape of GADT one finds for request types
module Request =
  /// The constructors must be kept private, so that we can refine the types of
  /// the introduction rules.
  type T<'a> =
    private
    | FileExists' of string
    | ReadText' of string
    | GetCwd'