libinput-rs 0.3.4

100% drop-in Rust replacement for the libinput 1.31.3 C ABI and tools
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

module ButtonLifecycle where

open import Agda.Builtin.Equality

data State : Set where
  up down : State

data Input : Set where
  press release disconnect : Input

data Output : Set where
  silent pressed released : Output

record Result : Set where
  constructor result
  field
    state : State
    output : Output

step : State -> Input -> Result
step up press = result down pressed
step down press = result down silent
step up release = result up silent
step down release = result up released
step up disconnect = result up silent
step down disconnect = result up released

duplicatePressIsSilent : step down press ≡ result down silent
duplicatePressIsSilent = refl

unmatchedReleaseIsSilent : step up release ≡ result up silent
unmatchedReleaseIsSilent = refl

lostReleaseRecovery : step down release ≡ result up released
lostReleaseRecovery = refl

disconnectBalancesPress : step down disconnect ≡ result up released
disconnectBalancesPress = refl