From 021f77afce66ad03b492e085385783cfb7be1cef Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Sat, 7 Sep 2024 11:59:00 +0200
Subject: [PATCH] push temporary tests

---
 tests/Compilation/positive/test082.juvix | 16 ++++++++++++++++
 tests/Compilation/positive/test083.juvix | 23 +++++++++++++++++++++++
 2 files changed, 39 insertions(+)
 create mode 100644 tests/Compilation/positive/test082.juvix
 create mode 100644 tests/Compilation/positive/test083.juvix

diff --git a/tests/Compilation/positive/test082.juvix b/tests/Compilation/positive/test082.juvix
new file mode 100644
index 0000000000..7cb089a7d8
--- /dev/null
+++ b/tests/Compilation/positive/test082.juvix
@@ -0,0 +1,16 @@
+module test082;
+
+trait
+type Suc (a : Type) := mkSuc a;
+
+trait
+type Zero := mkZero;
+
+trait
+type Add (a : Type) (b : Type) := mkAdd a b;
+
+instance
+addZeroI {B} {b : B} : Add Zero B := mkAdd mkZero b;
+
+instance
+addSucI {B} {b : B} {{Add Zero B}} : Add (Suc Zero) B := mkAdd (mkSuc mkZero) b;
diff --git a/tests/Compilation/positive/test083.juvix b/tests/Compilation/positive/test083.juvix
new file mode 100644
index 0000000000..22c872a66f
--- /dev/null
+++ b/tests/Compilation/positive/test083.juvix
@@ -0,0 +1,23 @@
+module test083;
+
+trait
+type Suc (a : Type) := mkSuc a;
+
+trait
+type Zero := mkZero;
+
+trait
+type Add (a : Type) (b : Type) := mkAdd a b;
+
+trait
+type Add' (a : Type) (b : Type) := mkAdd' a b;
+
+
+instance
+addZeroI {B} {b : B} : Add Zero B := mkAdd mkZero b;
+
+instance
+addSucI' {B} {b : B} {{Add' (Suc Zero) B}} : Add (Suc Zero) B := mkAdd (mkSuc mkZero) b;
+
+instance
+addSucI {B} {b : B} {{Add Zero B}} : Add (Suc Zero) B := mkAdd (mkSuc mkZero) b;