Changeset 276

Timestamp:

Nov 24, 2010, 4:16:02 PM (9 years ago)

Author:

mulligan

Message:

Messed up a file.

File:

• Deliverables/D4.1/Matita/Status.ma (modified) (1 diff)

Deliverables/D4.1/Matita/Status.ma

@@ -6 +6 @@
 include "Arithmetic.ma".
 include "BitVectorTrie.ma".
+
+ndefinition Time ≝ Nat.
+
+ninductive SerialBufferType: Type[0] ≝
+  Eight: Byte → SerialBufferType
+| Nine: Bit → Byte → SerialBufferType.
+
+ninductive LineType: Type[0] ≝
+  P1: Byte → LineType
+| P3: Byte → LineType
+| SerialBuffer: SerialBufferType → LineType.
+
+(* What is a continuation, now? *)
 
 ninductive SFR8051: Type[0] ≝