From 71f7527b6ef5f0a993249db444ca320ed143f31d Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Sat, 29 Aug 2026 12:02:07 +0200
Subject: Point free

---
 server/formal/period_seq.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'server/formal')

diff --git a/server/formal/period_seq.v b/server/formal/period_seq.v
index 705e505..8433bc6 100644
--- a/server/formal/period_seq.v
+++ b/server/formal/period_seq.v
@@ -13,9 +13,8 @@ Record period_seq :=
 *)
 
 Definition period_seq := list ne_period.
-
-Definition period_seq_nf (ps : period_seq) :=
-  Sorted period_before ps.
+Definition period_seq_nf : period_seq → Prop :=
+  Sorted period_before.
 
 Instance period_seq_elem_of : ElemOf timestamp period_seq :=
   λ t, Exists (λ p, t ∈ p).
-- 
cgit v1.3