Commit 8f1acb74 authored by Jan's avatar Jan

NEW: Now with strange typing error.

parent 1d29427d
Pipeline #11064 failed with stage
in 0 seconds
......@@ -22,7 +22,7 @@ Notation tokens sts := (set (token sts)).
(** * Theory and definitions *)
Section sts.
Context {sts : stsT}.
Context {sts : stsT}.
(** ** Step relations *)
Inductive step : relation (state sts * tokens sts) :=
......@@ -33,16 +33,19 @@ Notation steps := (rtc step).
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
(* Probably equivalent definition: (\mathcal{L}(s') ## T) ∧ s \rightarrow s' *)
| Frame_step T1 T2 :
T1 ## tok s1 T step (s1,T1) (s2,T2) frame_step T s1 s2.
T1 ## tok s1 T step (s1,T1) (s2,T2) frame_step T s1 s2.
Notation frame_steps T := (rtc (frame_step T)).
(** ** Closure under frame steps *)
Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
closed_disjoint s : s S tok s ## T;
closed_step s1 s2 : s1 S frame_step T s1 s2 s2 S
}.
}.
Definition up (s : state sts) (T : tokens sts) : states sts :=
{[ s' | frame_steps T s s' ]}.
Definition up_set (S : states sts) (T : tokens sts) : states sts :=
S = λ s, up s T.
......
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