mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-18 02:11:32 +03:00
23 lines
535 B
Idris
23 lines
535 B
Idris
|
import Data.Vect
|
||
|
|
|
||
|
|
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||
|
|
append xs ys = ?append_rhs
|
||
|
|
|
||
|
|
data DoorState = Open | Closed
|
||
|
|
|
||
|
|
data Door : DoorState -> Type where
|
||
|
|
MkDoor : (doorId : Int) -> Door st
|
||
|
|
|
||
|
|
openDoor : (1 d : Door Closed) -> Door Open
|
||
|
|
closeDoor : (1 d : Door Open) -> Door Closed
|
||
|
|
|
||
|
|
newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()
|
||
|
|
deleteDoor : (1 d : Door Closed) -> IO ()
|
||
|
|
|
||
|
|
doorProg : IO ()
|
||
|
|
doorProg
|
||
|
|
= newDoor $ \d =>
|
||
|
|
let d' = openDoor d
|
||
|
|
d'' = closeDoor d' in
|
||
|
|
deleteDoor d''
|