Permalink
Browse files

bintree-proba.agda

  • Loading branch information...
1 parent 655a42b commit 85cbb9d9644ad82149497406dd594b410e246115 @np np committed Apr 20, 2012
Showing with 10 additions and 0 deletions.
  1. +10 −0 bintree-proba.agda
View
@@ -0,0 +1,10 @@
+module bintree-proba
+ ([0,1] : Set)
+where
+
+open import Data.Nat
+open import Data.Bits
+
+data Tree : ℕ → Set where
+ leaf : {n} Bits n Tree n
+ fork : {n} (proba : [0,1]) (left right : Tree n) Tree (1 + n)

0 comments on commit 85cbb9d

Please sign in to comment.