diff --git a/tests/DepRecord.newt b/tests/DepRecord.newt new file mode 100644 index 0000000..7f3a1bd --- /dev/null +++ b/tests/DepRecord.newt @@ -0,0 +1,16 @@ +module DepRecord + +import Prelude + +infixr 6 _:-_ +data Vect : (0 n : Nat) → (0 a : U) → U where + VNil : ∀ a. Vect Z a + _:-_ : ∀ k a. a → Vect k a → Vect (S k) a + + +data Foo : U where + Bar : {n : Nat} → Vect n Int → Foo + +record DepPair where + n : Nat + stuff : Vect n Int