From 14a52d3f08a53fccda2b6eff614f00111cdf55f8 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 3 Jun 2020 13:33:48 +0200
Subject: [PATCH] Adding test for dependent types

---
 tests/vect.lp | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 tests/vect.lp

diff --git a/tests/vect.lp b/tests/vect.lp
new file mode 100644
index 0000000..865eee4
--- /dev/null
+++ b/tests/vect.lp
@@ -0,0 +1,8 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.deptype
+require open personoj.encodings.prenex
+
+symbol nat: θ {|set|}
+symbol vect: ϕ (∀K (λ_, scheme_k (nat *> {|set|})))
+assert vect: Set → η nat → Set
-- 
GitLab