rdbuf

module Leftpad

open FStar.List.Tot

val replicate : #a:eqtype -> n:nat -> x:a -> out:list a{length out == n /\ count x out == length out}
let rec replicate #a n x =
	if n = 0 then []
	else x :: replicate (n - 1) x

val leftpad : #a:eqtype -> n:nat -> x:a -> in_:list a -> out:list a{

rdbuf

module MergeSort

type nat = n:int{n>=0}

val length : l:list 'a -> nat
let rec length l = match l with
	| [] -> 0
	| hd :: tl -> 1 + length tl

val count : #a:eqtype -> x:a -> l:list a -> res:nat{res <= length l}

rdbuf

C++

1. PEGTL
2. Asio
3. libfmt
4. range-v3
5. HElib
6. owickstrom/hyper
7. matt-42/silicon
8. zaphoyd/websocketpp
9. catchorg/Clara

rdbuf

Ground

Nixos, ext4 under luks2 on lvm, luks encrypted boot [1], apparmor, sleep & hibernation support.

Monitor (primarily disk state) & send local mails & check up on zsh login.

Future: RAID 1, deniable encryption.

Userspace

Daily used apps go through the global config. All the rest goes through nix-shell, zero nix-env -i. Screen locking. Apparmor.

rdbuf

namespace ignore_access_rights {
template<class Ptr, int Id>
Ptr result = nullptr;
template<class Ptr, Ptr Target, int Id>
struct apply {
    struct exec { exec() { result<Ptr, Id> = Target; } };
    static exec var;
};
template<typename Ptr, Ptr Target, int Id> 
typename apply<Ptr, Target, Id>::exec apply<Ptr, Target, Id>::var;

rdbuf

{-# LANGUAGE GADTs #-}

import Control.Monad (replicateM, ap)
import Data.List (minimumBy)
import Data.Function (on)
import Data.Monoid

data Vec a where
    Vec :: Integral a => a -> a -> Vec a

rdbuf

{-# LANGUAGE OverloadedStrings #-}

import Text.Parsec hiding (token)
import Options.Applicative hiding (many, (<|>), option)
import Data.Monoid
import Data.Maybe
import Control.Monad
import Data.Text.Lazy (unpack)
import Formatting (format, (%), (%.))
import Formatting.Formatters (left, int)

rdbuf

import Data.Monoid ((<>))
import Data.Tuple (fst, snd, swap)
import Data.List (splitAt, isPrefixOf)
import Data.Char (isAlpha)
import Data.Bifunctor (bimap)
import Control.Monad ((=<<), join)
import Control.Applicative (liftA2)

-- Algorithmically, it's bad.
-- It's more of a practice in writing point-free code.

rdbuf

#include <stdio.h>

#include "strhead.h"

void print(const struct str_* s) {
    printf("i = %i\n"
           "d = %lf\n", s->i, s->d);
}

int main() {

rdbuf

#include <iostream>
#include <utility>

template<class Integer>
Integer nth_fib(const size_t n) {
  Integer prev = 1, cur = 1;

  if (n < 3) {
    cur = [&]() -> Integer {
      switch (n) {