summaryrefslogtreecommitdiff
path: root/test-suite/output/ArgumentsScope.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/ArgumentsScope.out')
-rw-r--r--test-suite/output/ArgumentsScope.out56
1 files changed, 56 insertions, 0 deletions
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
new file mode 100644
index 00000000..6643c142
--- /dev/null
+++ b/test-suite/output/ArgumentsScope.out
@@ -0,0 +1,56 @@
+a : bool -> bool
+
+Argument scope is [bool_scope]
+Expands to: Variable a
+b : bool -> bool
+
+Argument scope is [bool_scope]
+Expands to: Variable b
+negb'' : bool -> bool
+
+Argument scope is [bool_scope]
+negb'' is transparent
+Expands to: Constant Top.A.B.negb''
+negb' : bool -> bool
+
+Argument scope is [bool_scope]
+negb' is transparent
+Expands to: Constant Top.A.negb'
+negb : bool -> bool
+
+Argument scope is [bool_scope]
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+a : bool -> bool
+
+Expands to: Variable a
+b : bool -> bool
+
+Expands to: Variable b
+negb : bool -> bool
+
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+negb' : bool -> bool
+
+negb' is transparent
+Expands to: Constant Top.A.negb'
+negb'' : bool -> bool
+
+negb'' is transparent
+Expands to: Constant Top.A.B.negb''
+a : bool -> bool
+
+Expands to: Variable a
+negb : bool -> bool
+
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+negb' : bool -> bool
+
+negb' is transparent
+Expands to: Constant Top.negb'
+negb'' : bool -> bool
+
+negb'' is transparent
+Expands to: Constant Top.negb''