push temporary tests

anoma · Sep 7, 2024 · 021f77a · 021f77a
1 parent e9a6009
commit 021f77a
Show file tree

Hide file tree

Showing 2 changed files with 39 additions and 0 deletions.
diff --git a/tests/Compilation/positive/test082.juvix 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
@@ -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;