diff options
| author | Rutger Broekhoff | 2026-08-29 12:02:07 +0200 |
|---|---|---|
| committer | Rutger Broekhoff | 2026-08-29 12:02:07 +0200 |
| commit | 71f7527b6ef5f0a993249db444ca320ed143f31d (patch) | |
| tree | 4a854c7f619663f0ec967d8a03dbf2e9604c089e /server/formal | |
| parent | 52b3cd46c76fd4be18aeb8422a08a073484b9fad (diff) | |
| download | routemon-71f7527b6ef5f0a993249db444ca320ed143f31d.tar.gz routemon-71f7527b6ef5f0a993249db444ca320ed143f31d.zip | |
Point free
Diffstat (limited to 'server/formal')
| -rw-r--r-- | server/formal/period_seq.v | 5 |
1 files changed, 2 insertions, 3 deletions
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 := | |||
| 13 | *) | 13 | *) |
| 14 | 14 | ||
| 15 | Definition period_seq := list ne_period. | 15 | Definition period_seq := list ne_period. |
| 16 | 16 | Definition period_seq_nf : period_seq → Prop := | |
| 17 | Definition period_seq_nf (ps : period_seq) := | 17 | Sorted period_before. |
| 18 | Sorted period_before ps. | ||
| 19 | 18 | ||
| 20 | Instance period_seq_elem_of : ElemOf timestamp period_seq := | 19 | Instance period_seq_elem_of : ElemOf timestamp period_seq := |
| 21 | λ t, Exists (λ p, t ∈ p). | 20 | λ t, Exists (λ p, t ∈ p). |