jozefg

Operator P : (0).
[P(N)] =def= [natrec(N; unit; _._.void)].

Theorem one-not-zero : [not(=(zero; succ(zero); nat))] {
  auto;
  assert [P(succ(zero))];
  aux {
    unfold <P>; hyp-subst ← #1 [h.natrec(h; _; _._._)];
    reduce; auto
  };

jozefg

### Keybase proof

I hereby claim:

  * I am jozefg on github.
  * I am jozefg (https://keybase.io/jozefg) on keybase.
  * I have a public key whose fingerprint is F6CF 1EA2 013C 8700 D24B  030D D5DC A663 AAE6 2FAE

To claim this, I am signing this object:

jozefg

{-# LANGUAGE RecordWildCards #-}
module Unify where
import Control.Monad.Logic
import qualified Data.Map as M

type Id = Integer
type Atom = String

data Term = Var Id
          | Atom Atom

jozefg

term : type.
and : term -> term -> term.
or  : term -> term -> term.
imp : term -> term -> term.
top : term.

hyp : term -> type.

true : term -> type.
init : true A

jozefg

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
module Main where
import Data.Foldable
import Data.Traversable
import Data.Monoid

jozefg

use std::io::stdin;

fn fizzbuzz (n : int) -> String {
    match (n % 3 == 0, n % 5 == 0) {
        (true, true) => "FizzBuzz".to_string(),
        (false, true) => "Fizz".to_string(),
        (true, false) => "Buzz".to_string(),
        (false, false) => n.to_string()
    }
}

jozefg

enum Tree<A> {
    Leaf(A),
    Node(Box<Tree<(A, A)>>)
}

fn size<A>(t : &Tree<A>) -> int {
    match t {
        &Leaf(_) => 1,
        &Node(box ref t) => size(t)
    }

jozefg

{-# LANGUAGE LambdaCase #-}
module LambdaPi where
import           Control.Applicative hiding (Const)
import           Control.Monad       (guard)
import           Control.Monad.Gen
import           Control.Monad.Trans
import qualified Data.Map            as M

data IExpr = Var Int
           | App IExpr CExpr

jozefg

nat : type.
s   : nat -> nat.
z   : nat.

bool  : type.
true  : bool.
false : bool.

plus : nat -> nat -> nat -> type.
%mode plus +N +M -R.

jozefg

module queue
import Data.Vect

-- Here's the port of the Liquid Haskell blog post on amortized
-- queues. The tricksy bit is that the "amortized" bit depends on
-- laziness. This means that while in the REPL (where Idris is lazy)
-- this is reasonably efficient. It compiles absolutely horribly
-- though because each time push or pop something we rotate the whole
-- damned thing.