dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

add missing function, todo items

Browse Source
This commit is contained in:
Steve Dunham
2024-12-03 16:41:33 -08:00
parent f573736b7f
commit ee50677d4b
2 changed files with 16 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
TODO.md
View File

@@ -2,6 +2,9 @@
## TODO ## TODO
- [x] Put worker in iframe on safari - [x] Put worker in iframe on safari
- [ ] Warnings or errors for missing definitions
- [ ] Warnings or errors for unused cases
- Important when misspelled constructors become pattern vars
- [ ] 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
@@ -13,6 +16,7 @@
- [x] make $ special - [x] make $ special
- Makes inference easier, cleaner output, and allows `foo $ \ x => ...` - Makes inference easier, cleaner output, and allows `foo $ \ x => ...`
- remove hack from Elab.infer - remove hack from Elab.infer
- [ ] `$` no longer works inside ≡⟨ ⟩ sort out how to support both that and `$ \ x => ...`
- [ ] Support @ on the LHS - [ ] Support @ on the LHS
- [ ] records - [ ] records
- [ ] rework unify case tree - [ ] rework unify case tree
@@ -22,6 +26,7 @@
- Meta hasn't been solved yet. It's Normal, but maybe our delayed solving of Auto plays into it. Idris will peek at LHS of CaseAlts to guess the type if it doesn't have one. - Meta hasn't been solved yet. It's Normal, but maybe our delayed solving of Auto plays into it. Idris will peek at LHS of CaseAlts to guess the type if it doesn't have one.
- [ ] Can't skip an auto. We need `{{_}}` to be auto or `%search` syntax. - [ ] Can't skip an auto. We need `{{_}}` to be auto or `%search` syntax.
- [x] add filenames to FC - [x] add filenames to FC
- [ ] Add full ranges to FC
- [x] maybe use backtick for javascript so we don't highlight strings as JS - [x] maybe use backtick for javascript so we don't highlight strings as JS
- [ ] add namespaces - [ ] add namespaces
- [x] dead code elimination - [x] dead code elimination

11
playground/samples/Reasoning.newt
View File

@@ -94,6 +94,17 @@ reverse (x :: xs) = reverse xs ++ (x :: Nil)
-- concatenation is associative -- concatenation is associative
++-associative : ∀ A. (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs ++-associative : ∀ A. (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
++-associative Nil ys zs = Refl
++-associative (x :: xs) ys zs =
begin
(x :: xs) ++ (ys ++ zs)
≡⟨⟩
x :: (xs ++ (ys ++ zs))
≡⟨ cong (_::_ x) (++-associative xs ys zs) ⟩
x :: ((xs ++ ys) ++ zs)
≡⟨⟩
(x :: xs ++ ys) ++ zs
∎
-- reverse distributes over ++, but switches order -- reverse distributes over ++, but switches order
reverse-++-distrib : ∀ A. (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs reverse-++-distrib : ∀ A. (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs