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

log issue

Browse Source
This commit is contained in:
Steve Dunham
2025-11-17 09:34:13 -08:00
parent f04813519c
commit 30ff87c2e2
2 changed files with 15 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
TODO.md
View File

@@ -1,7 +1,6 @@
## TODO ## TODO
- [x] `newt/Problem.newt` coverage issues
- [ ] Maybe make the editor json more compact - [ ] Maybe make the editor json more compact
- [ ] Remove erased args from primitive functions - [ ] Remove erased args from primitive functions
- But we need separate `+` functions rather than the magic `∀ a. a -> a -> a` to support other backends - But we need separate `+` functions rather than the magic `∀ a. a -> a -> a` to support other backends
@@ -13,6 +12,7 @@
- Removes assumptions of hack in Compile.newt, but might not support other backends - Removes assumptions of hack in Compile.newt, but might not support other backends
- Alternate solution would be to pull from Prelude and hard code for all backends - Alternate solution would be to pull from Prelude and hard code for all backends
- POper added to physical syntax types, but not implemented - POper added to physical syntax types, but not implemented
- [ ] Fix issue with erasure checking: `tests/aside/Quantity.newt`.
- [x] Remove erased fields from constructor data - [x] Remove erased fields from constructor data
- [ ] Teach magic nat / magic enum about erased args - [ ] Teach magic nat / magic enum about erased args
- [x] Update LiftLambda.newt for arg removal changes - [x] Update LiftLambda.newt for arg removal changes

14
tests/aside/Quantity.newt Normal file
View File

@@ -0,0 +1,14 @@
module Quantity
import Prelude
foo : Nat → Nat
foo x = x
-- This should fail to compile
bar : ∀ x. Nat
bar {x} = foo x
main : IO Unit
main = printLn $ bar {S Z}