tweak to day3
This commit is contained in:
2
TODO.md
2
TODO.md
@@ -1,10 +1,12 @@
|
|||||||
|
|
||||||
## TODO
|
## TODO
|
||||||
|
|
||||||
|
- [x] Put worker in iframe on safari
|
||||||
- [ ] if we're staying with this version of auto, we might need to list candidates and why they're rejected. e.g. I had a bifunctor fail to solve because the right answer unblocked a Foo vs IO Foo mismatch
|
- [ ] if we're staying with this version of auto, we might need to list candidates and why they're rejected. e.g. I had a bifunctor fail to solve because the right answer unblocked a Foo vs IO Foo mismatch
|
||||||
- [ ] literals for double
|
- [ ] literals for double
|
||||||
- [ ] default failing case for constructor matching
|
- [ ] default failing case for constructor matching
|
||||||
- [ ] Add icit to Lam (see `check` for details)
|
- [ ] Add icit to Lam (see `check` for details)
|
||||||
|
- [ ] add jump to definition magic to vscode extension
|
||||||
- [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
|
- [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
|
||||||
- [x] deconstructing `let` (and do arrows)
|
- [x] deconstructing `let` (and do arrows)
|
||||||
- [x] Fix string printing to be js instead of weird Idris strings
|
- [x] Fix string printing to be js instead of weird Idris strings
|
||||||
|
|||||||
@@ -114,7 +114,7 @@ _>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
|
|||||||
ma >>= amb = bind ma amb
|
ma >>= amb = bind ma amb
|
||||||
|
|
||||||
_>>_ : {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
|
_>>_ : {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
|
||||||
ma >> mb = mb
|
ma >> mb = ma >>= (\ _ => mb)
|
||||||
|
|
||||||
join : ∀ m. {{Monad m}} {0 a} → m (m a) → m a
|
join : ∀ m. {{Monad m}} {0 a} → m (m a) → m a
|
||||||
join mma = mma >>= id
|
join mma = mma >>= id
|
||||||
@@ -622,3 +622,8 @@ isNothing _ = False
|
|||||||
instance Bifunctor _×_ where
|
instance Bifunctor _×_ where
|
||||||
bimap f g (a,b) = (f a, g b)
|
bimap f g (a,b) = (f a, g b)
|
||||||
|
|
||||||
|
instance Functor IO where
|
||||||
|
map f a = bind a $ \ a => pure (f a)
|
||||||
|
|
||||||
|
uncurry : ∀ a b c. (a -> b -> c) -> (a × b) -> c
|
||||||
|
uncurry f (a,b) = f a b
|
||||||
|
|||||||
@@ -4,17 +4,12 @@ import Prelude
|
|||||||
import Node
|
import Node
|
||||||
import Aoc
|
import Aoc
|
||||||
|
|
||||||
uncurry : ∀ a b c. (a -> b -> c) -> (a × b) -> c
|
|
||||||
uncurry f (a,b) = f a b
|
|
||||||
|
|
||||||
Parser : U → U
|
Parser : U → U
|
||||||
Parser a = List Char → Maybe (a × List Char)
|
Parser a = List Char → Maybe (a × List Char)
|
||||||
|
|
||||||
instance Monad Parser where
|
instance Monad Parser where
|
||||||
pure a = \ cs => Just (a, cs)
|
pure a = \ cs => Just (a, cs)
|
||||||
bind ma mab = \ cs => case ma cs of
|
bind ma mab = \ cs => ma cs >>= uncurry mab
|
||||||
Nothing => Nothing
|
|
||||||
Just (a,cs) => mab a cs
|
|
||||||
|
|
||||||
instance Alternative Parser where
|
instance Alternative Parser where
|
||||||
pa <|> pb = \ cs => case pa cs of
|
pa <|> pb = \ cs => case pa cs of
|
||||||
|
|||||||
1
aoc2024/Node.newt
Symbolic link
1
aoc2024/Node.newt
Symbolic link
@@ -0,0 +1 @@
|
|||||||
|
../aoc2023/Node.newt
|
||||||
1
aoc2024/Prelude.newt
Symbolic link
1
aoc2024/Prelude.newt
Symbolic link
@@ -0,0 +1 @@
|
|||||||
|
../aoc2023/Prelude.newt
|
||||||
Reference in New Issue
Block a user