From 1cc79bf55da07801ff2f530fb8a25675beab96e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Tue, 15 Oct 2024 09:57:19 +0200 Subject: [PATCH] fix compilation error after merge --- src/core/DY.Core.Trace.Base.fst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/core/DY.Core.Trace.Base.fst b/src/core/DY.Core.Trace.Base.fst index 6c7f284..1956090 100644 --- a/src/core/DY.Core.Trace.Base.fst +++ b/src/core/DY.Core.Trace.Base.fst @@ -401,7 +401,7 @@ val get_event_at_trace_forget_labels: tr:trace -> i:timestamp{i < length tr} -> Lemma ( length_trace_forget_labels tr; - get_event_at (trace_forget_labels tr) i == (fmap_trace_event (forget_label ()) (get_event_at tr i)) + get_event_at (trace_forget_labels tr) i == (fmap_trace_event forget_label (get_event_at tr i)) ) let rec get_event_at_trace_forget_labels tr i = length_trace_forget_labels tr; @@ -415,7 +415,7 @@ val event_at_trace_forget_labels: tr:trace -> i:timestamp -> ev:trace_event -> Lemma (requires event_at tr i ev) - (ensures event_at (trace_forget_labels tr) i (fmap_trace_event (forget_label ()) ev)) + (ensures event_at (trace_forget_labels tr) i (fmap_trace_event forget_label ev)) let event_at_trace_forget_labels tr i ev = length_trace_forget_labels tr; if i >= length tr then () @@ -427,10 +427,10 @@ val event_exists_trace_forget_labels: tr:trace -> ev:trace_event -> Lemma (requires event_exists tr ev) - (ensures event_exists (trace_forget_labels tr) (fmap_trace_event (forget_label ()) ev)) + (ensures event_exists (trace_forget_labels tr) (fmap_trace_event forget_label ev)) let event_exists_trace_forget_labels tr ev = eliminate exists i. event_at tr i ev - returns event_exists (trace_forget_labels tr) (fmap_trace_event (forget_label ()) ev) + returns event_exists (trace_forget_labels tr) (fmap_trace_event forget_label ev) with _. ( event_at_trace_forget_labels tr i ev )