Permalink
Browse files

Little spike file encoding http spec definitions as types directly

  • Loading branch information...
1 parent 7dcc217 commit 176867bea78f2cea2153e43544848c5e98fdd387 Larry Diehl committed May 23, 2010
Showing with 11 additions and 0 deletions.
  1. +11 −0 Lemmachine/Spike.agda
View
@@ -0,0 +1,11 @@
+module Lemmachine.Spike where
+open import Data.Fin
+open import Data.Digit
+
+-- 3.9 Quality Values
+
+DIGIT = Decimal
+
+data qvalue : DIGIT → DIGIT → DIGIT → Set where
+ zero : (d₁ d₂ d₃ : DIGIT) qvalue d₁ d₂ d₃
+ one : qvalue zero zero zero

0 comments on commit 176867b

Please sign in to comment.