From 84c400872430106aa1cbf8d2cbacf33baee7f97e Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Fri, 23 Jan 2026 08:53:49 -0800
Subject: [PATCH] check in test from dependent record fix

---
 tests/DepRecord.newt | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 tests/DepRecord.newt

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