From f2011d547227dfcadbdd93cd445db0f93c40579d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 6 Nov 2023 14:45:13 +0100
Subject: [PATCH] wip TC.declare to give attributes on the fly

---
 apps/tc/theories/wip.v | 26 +++++++++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/apps/tc/theories/wip.v b/apps/tc/theories/wip.v
index 610ce7173..a676988a6 100644
--- a/apps/tc/theories/wip.v
+++ b/apps/tc/theories/wip.v
@@ -50,4 +50,28 @@ Elpi Accumulate lp:{{
   main [trm New, trm Old] :-
     add-tc-db _ _ (alias New Old).
 }}.
-Elpi Typecheck.
\ No newline at end of file
+Elpi Typecheck.
+
+
+(*
+Elpi Command TC.declare.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
+Elpi Accumulate File create_tc_predicate.
+Elpi Accumulate lp:{{
+  main [indt-decl D] :-
+    attributes A,
+    coq.say A,
+    Opts => 
+      get-option "modes" [tt,ff,tt],
+    coq.env.add-indt D I,
+    coq.say I.
+}}.
+Elpi Typecheck.
+Elpi Export TC.declare.
+
+#[mode(i,i,o)] TC.declare
+  Class foo (A : Type) .
+*)