Commit 62aff812 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Properly define trace notation globally

parent 4e862e5a
......@@ -773,11 +773,8 @@ Fixpoint trace_app
fun c1 => ctrace_permute (trace_app c1 pref) perm
end c1.
Delimit Scope trace_scope with trace.
Bind Scope trace_scope with ChainTrace.
Infix "++" := trace_app (right associativity, at level 60) : trace_scope.
Infix "++" := trace_app (right associativity, at level 60).
Local Open Scope trace.
Definition trace_prefix
{from mid to : Environment}
{from_queue mid_queue to_queue : list Action}
......@@ -792,9 +789,6 @@ Definition trace_suffix
(full : ChainTrace from from_queue to to_queue) : Prop :=
exists prefix, full = prefix ++ suf.
Infix "`prefix_of`" := trace_prefix (at level 70) : trace_scope.
Infix "`suffix_of`" := trace_suffix (at level 70) : trace_scope.
Section Theories.
Lemma trace_app_refl_l
{from to from_queue to_queue}
......@@ -874,6 +868,12 @@ Class ChainBuilderType :=
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
End Blockchain.
Delimit Scope trace_scope with trace.
Bind Scope trace_scope with ChainTrace.
Infix "++" := trace_app (right associativity, at level 60) : trace_scope.
Infix "`prefix_of`" := trace_prefix (at level 70) : trace_scope.
Infix "`suffix_of`" := trace_suffix (at level 70) : trace_scope.
Arguments version {_ _ _ _ _ _ _}.
Arguments init {_ _ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _ _}.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment