Fix

Author: ajreynol

src/cmd_parser.cpp

@@ -182,7 +182,7 @@ bool CmdParser::parseNextCommand()
       }
       if (!params.empty())
       {
-        // parameters are quote arrows
+        // explicit parameters are quote arrows
         for (size_t i=0, nparams = params.size(); i<nparams; i++)
         {
           size_t ii = nparams-i-1;

tests/CMakeLists.txt

@@ -142,6 +142,7 @@ set(ethos_test_file_list
     overload-define.eo
     nested-requires.eo
     pairwise-singleton.eo
+    quote-opaque.eo
 )
 
 if(ENABLE_ORACLES)

tests/quote-opaque.eo

@@ -0,0 +1,38 @@
+(declare-type Int ())
+(declare-consts <numeral> Int)
+
+(declare-const @const (-> (! Int :opaque) (! Type :var T :opaque) T))
+
+
+
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(program substitute
+  ((T Type) (U Type) (S Type) (x S) (y S) (f (-> T U)) (a T) (z U))
+  (S S U) U
+  (
+  ((substitute x y x)     y)
+  ((substitute x y (f a)) (_ (substitute x y f) (substitute x y a)))
+  ((substitute x y z)     z)
+  )
+)
+
+
+(declare-rule eq-subs
+   ((f Bool) (a Bool) (b Bool))
+   :premises (f (= a b))
+   :args ()
+   :conclusion (substitute a b f)
+)
+
+(declare-const T Type)
+(declare-const U Type)
+(declare-const f (-> U T))
+(assume a1 (= (@const 1 T) (f (@const 1 U))))
+(assume a2 (= T U))
+; substitution will not impact the n within the opaque symbol
+(step a3 (= (@const 1 T) (f (@const 1 U))) :rule eq-subs :premises (a1 a2))
+
+
+
+;(declare-parameterized-const @pconst ((id Int :opaque) (T Type :opaque))