Skip to content

Instantly share code, notes, and snippets.

@deech

deech/indexed-natural-numbers.shen

Created February 28, 2013 13:11
Show Gist options
  • Save deech/5056607 to your computer and use it in GitHub Desktop.
Save deech/5056607 to your computer and use it in GitHub Desktop.
Download ZIP
Indexed natural numbers
Raw
indexed-natural-numbers.shen
(datatype natnum
if (integer? X)
if (> X -1)
________________
X : (natnum X);
(let A (+ X 1));
X : (natnum X);
__________
(+ X 1) : (natnum A);
(let A (- X 1));
(not (= X 0)) : verified; X : (natnum X);
_____________________________________
(- X 1) : (natnum A);)
(define plus
{(natnum X) --> (natnum Y) --> (natnum Z)}
0 X -> X
X Y -> (plus (- X 1) (+ Y 1)) where(not (= X 0)) )
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment