keleshev

#! /usr/bin/env ocaml

let fprintf = Format.fprintf

type t =
  | Tag of {name: string; attributes: (string * string) list; body: t list}
  | String of string

let format_attribute f (key, value) = fprintf f " %s=\"%s\"" key value

BekaValentine

import sys
from time import sleep
import random
import cursor



class Renderer:

  def __init__(self, width, height):

t0yv0

Require Import Utf8.

Inductive subtype (a b : Set) : Set :=
| ST : (a -> b) -> subtype a b.

Infix ":>" := subtype (at level 50).

Definition st {x y} f := ST x y f.

Definition unpack {a b : Set} (st : a :> b) :=

bobatkey

(* This is a demonstration of the use of the SML module system to
   encode (Generalized Algebraic Datatypes) GADTs via Church
   encodings. The basic idea is to use the Church encoding of GADTs in
   System Fomega and translate the System Fomega type into the module
   system. As I demonstrate below, this allows things like the
   singleton type of booleans, and the equality type, to be
   represented.

   This was inspired by Jon Sterling's blog post about encoding proofs
   in the SML module system:

Leonidas-from-XIV

module Let_syntax = struct
  let return = Lwt.return
  let (>>=) = Lwt.Infix.(>>=)
  let (>>|) = Lwt.Infix.(>|=)
  module Let_syntax = struct
    let bind m ~f = Lwt.bind m f
  end
end

jozefg

signature TYPEINFER =
sig
    type tvar =  int
    datatype monotype = TBool
                      | TArr of monotype * monotype
                      | TVar of tvar
    datatype polytype = PolyType of int list * monotype
    datatype exp = True
                 | False
                 | Var of int

david-christiansen

module FizzBuzzC

%default total

-- Dependently typed FizzBuzz, constructively

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy 0
  Fizz : Fizzy n -> Fizzy (3 + n)

zaphar

-module(date_util).
-compile(export_all).

epoch() ->
    now_to_seconds(now())
.   
    
epoch_hires() ->
    now_to_seconds_hires(now())
.   

chambart

type zero = unit
type 'a succ = unit -> 'a
type one = zero succ

type 'a plus_1 = 'a succ
type 'a plus_2 = 'a plus_1 plus_1
type 'a plus_4 = 'a plus_2 plus_2
type 'a plus_8 = 'a plus_4 plus_4

Drup

type ('ty,'v) t =
  | Nil : ('v, 'v) t
  | Cons : 'a * ('ty, 'v) t -> ('a -> 'ty, 'v) t

let cons x l = Cons (x,l)

let plus1 l = Cons ((),l)

let one x = Cons (x,Nil)