jonsterling

open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd1 where

----------------------------------------------------------------------

add : (m n : ℕ) → ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add m n = elimℕ (λ m' → ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)

jonsterling

[0.066684s] Checked test/success/V-types.prl
[0.022747s] Checked test/success/bool-fhcom-without-open-eval.prl
[0.009820s] Checked test/success/bool-pair-test.prl
[0.010696s] Checked test/success/dashes-n-slashes.prl
[0.009144s] Checked test/success/decomposition.prl
[0.006263s] Checked test/success/discrete-types.prl
[0.013531s] Checked test/success/empty.prl
[0.009508s] Checked test/success/equality-elim.prl
[0.017783s] Checked test/success/equality.prl
[0.017168s] Checked test/success/fcom-types.prl

jonsterling

Keybase proof

I hereby claim:

• I am jonsterling on github.
• I am jonsterling (https://keybase.io/jonsterling) on keybase.
• I have a public key whose fingerprint is 0D26 4B16 F650 0D8A CFB1 A781 2FC8 9E5C B6AC C521

To claim this, I am signing this object:

jonsterling

#!/usr/bin/python
# -*- coding: latin-1 -*-

import urwid
import json
import subprocess

class TaskWarrior(object):

    def pending_tasks(self):

jonsterling

Nuprl_functional = 
λ _top_assumption_ : nat,
(λ (_evar_0_ : (λ n : nat, matrix_functional (Nuprl n)) 0)
 (_evar_0_0 : ∀ n : nat, (λ n0 : nat, matrix_functional (Nuprl n0)) (S n)),
 match
   _top_assumption_ as n
   return ((λ n0 : nat, matrix_functional (Nuprl n0)) n)
 with
 | 0 => _evar_0_

jonsterling

\documentclass{article}
\usepackage{libertine}
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}
\usepackage{amsmath, amssymb, proof, microtype, hyperref}
\usepackage{mathpartir} % for mathpar, not for proofs

\usepackage{perfectcut}
\newcommand\Parens[1]{\perfectparens{#1}}
\newcommand\Squares[1]{\perfectbrackets{#1}}

jonsterling

#import <Foundation/Foundation.h>
#import <CoreGraphics/CoreGraphics.h>
#import <objc/message.h>
#import <string>
#import <map>
#import <typeinfo>

#define $(value) box<typeof(value)>(value)

using namespace std;

jonsterling

signature EQ =
sig
  type t
  val eq : t * t -> bool
end

signature SHOW =
sig
  type t
  val toString : t -> string

jonsterling

module experiment where

open import Agda.Primitive
open import Prelude.List
open import Prelude.Size
open import Prelude.Monoidal
open import Prelude.Monad
open import Prelude.Functor
open import Prelude.Natural
open Size using (∞)

jonsterling

id : type.
id/z : id.
id/s : id -o id.

answer : type.
yes : answer.
no : answer.

id/eq? : id -> id -> answer -> type.
id/eq/z/z : id/eq? id/z id/z yes.