TethysSvensson

use std::marker::PhantomData;

pub struct NegOne;
pub struct Zero;

pub struct Bit0<N>(PhantomData<N>);
pub struct Bit1<N>(PhantomData<N>);

macro_rules! t {
    ($accum:ty) => {

TethysSvensson

struct NegOne;
struct Zero;

struct Bit0<N>(PhantomData<N>);
struct Bit1<N>(PhantomData<N>);

type One = Bit1<Zero>;
type NegTwo = Bit0<NegOne>;

trait Integer {

TethysSvensson

struct NegOne;
struct Zero;

struct Bit0<N>(PhantomData<N>);
struct Bit1<N>(PhantomData<N>);

type One = Bit1<Zero>;
type NegTwo = Bit1<NegOne>;

trait Integer {

TethysSvensson

struct NegOne;
struct Zero;

struct Shift<N>(PhantomData<N>);
struct Shift1<N>(PhantomData<N>);

type One = Shift1<Zero>;

trait Integer {
    const VALUE: i128;

TethysSvensson

{ pkgs, writeScriptBin, hacksaw, shotgun, xclip }:

writeScriptBin "screenshot" ''
  #!${pkgs.bash}/bin/sh

  set -e

  file=$(date +/tmp/screenshot-%F-%H%M%S.png)
  if [[ "$1" = "full" ]]; then
    ${shotgun}/bin/shotgun $file

TethysSvensson

#[derive(Copy, Clone)]
enum LinkedList<'a> {
    Nil,
    Cons(u8, &'a LinkedList<'a>),
}

struct LinkedListIter<'a> {
    list: LinkedList<'a>,
}

TethysSvensson

Keybase proof

I hereby claim:

• I am tethyssvensson on github.
• I am idolfhatler (https://keybase.io/idolfhatler) on keybase.
• I have a public key ASA_aryPlRjMh1wwOTLM6sgIjvlyeyx6iPPZg75T7JZkIwo

To claim this, I am signing this object:

TethysSvensson

use flatbuffers::{Vector, Follow};

fn first<'a, T: Follow<'a> + 'a>(v: Vector<'a, T>) -> Option<T::Inner> {
    if v.len() > 0 {
        Some(v.get(0))
    } else {
        None
    }
}

TethysSvensson

module Test where

open import Function using (id ; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Data.Maybe

record RawFunctor (F : Set → Set) : Set₁ where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

TethysSvensson

module Test where

open import Function using (id ; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

record RawFunctor (F : Set → Set) : Set₁ where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

open RawFunctor {{...}} public