update basic-consts test

lcnr · Apr 11, 2022 · 2a9fadc · 2a9fadc
1 parent fe3e563
commit 2a9fadc
Showing 1 changed file with 19 additions and 0 deletions.
diff --git a/src/decl/test/basic-consts.rkt b/src/decl/test/basic-consts.rkt
@@ -21,7 +21,26 @@
     (CrateDecl (term (TheCrate (crate (TraitDecl AdtDecl_Foo ConstDecl_Malformed)))))
     (Env (term (env-for-crate-decl CrateDecl)))
     )
+   (traced '()
+           (decl:test-cannot-prove
+            Env
+            (crate-ok-goal (CrateDecl) CrateDecl)))
+   )
 
+  ;; Program:
+  ;;
+  ;; trait Debug { }
+  ;; struct Foo<T: Debug> { }
+  ;; const WF<T: Debug>: Foo<T>;
+  (redex-let*
+   formality-decl
+
+   ((TraitDecl (term (Debug (trait ((TyKind Self)) () ()))))
+    (AdtDecl_Foo (term (Foo (struct ((TyKind T)) ((Implemented (Debug (T)))) ((Foo ()))))))
+    (ConstDecl_Wf (term (Wf (const ((TyKind T)) ((Implemented (Debug (T)))) (TyRigid Foo (T))))))
+    (CrateDecl (term (TheCrate (crate (TraitDecl AdtDecl_Foo ConstDecl_Wf)))))
+    (Env (term (env-for-crate-decl CrateDecl)))
+    )
    (traced '()
            (decl:test-can-prove
             Env