We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent dece463 commit bc9740bCopy full SHA for bc9740b
apps/derive/tests/test_derive.v
@@ -164,3 +164,7 @@ Inductive wimpls {A} `{rtree A} := Kwi (x:A) (y : x = x) : wimpls | Kwa.
164
About wimpls.wimpls.
165
About wimpls.Kwi.
166
Check Kwi _ (refl_equal 3).
167
+
168
+From Coq Require Ascii.
169
170
+#[only(param2)] derive Ascii.ascii.
apps/derive/theories/derive/param2.v
@@ -54,8 +54,8 @@ Elpi Accumulate lp:{{
54
Elpi Typecheck.
55
56
(* hook into derive *)
57
-Elpi Accumulate derive Db derive.param2.db.
58
Elpi Accumulate derive File param2.
+Elpi Accumulate derive Db derive.param2.db.
59
Elpi Accumulate derive lp:{{
60
61
derivation T N (derive "param2" (derive.param2.main T N) (param-done T)).
0 commit comments