-
Notifications
You must be signed in to change notification settings - Fork 0
/
Main.lean
29 lines (24 loc) · 867 Bytes
/
Main.lean
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
import «HashBrown»
open HashBrown
open HashMap HashSet HashState
def constructMap (x : Nat) (acc : HashMap Nat String) : HashMap Nat String :=
match x with
| Nat.zero => acc
| Nat.succ n => constructMap n <| acc.insert x <| toString x
def constructSet (x : Nat) (acc : SeededHashSet FxMixer Nat := default) : SeededHashSet FxMixer Nat :=
match x with
| Nat.zero => acc.insert x
| Nat.succ n => constructSet n <| acc.insert x
partial def hashSet (stdin: IO.FS.Stream) (output: IO.FS.Stream): StateT (SeededHashSet FxMixer String) IO Unit := do
let map ← get
let line ← stdin.getLine
let str := line.trim
if str.length == 0
then output.putStrLn s!"{map}"
else
modify (·.insert str)
hashSet stdin output
def main : IO Unit := do
let stdin <- IO.getStdin
let stdout <- IO.getStdout
hashSet stdin stdout |>.run' default