Add some sketches of Fathom’s core in Idris 2 #391
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
brendanzab
force-pushed
the
expriments/idris
branch
from
7a78446 to
5bc6398
Compare
brendanzab
force-pushed
the
expriments/idris
branch
from
a214fc7 to
315acb1
Compare
brendanzab
commented
Aug 25, 2022
brendanzab
force-pushed
the
expriments/idris
branch
from
0bceb3c to
9f0cd55
Compare
brendanzab
force-pushed
the
expriments/idris
branch
2 times, most recently
from
a2eb43b to
6ffd327
Compare
brendanzab
force-pushed
the
expriments/idris
branch
2 times, most recently
from
a7c7bb6 to
a379dea
Compare
brendanzab
force-pushed
the
expriments/idris
branch
3 times, most recently
from
30e8d0e to
4bd0ba6
Compare
brendanzab
force-pushed
the
expriments/idris
branch
from
4bd0ba6 to
4e01ddc
Compare
brendanzab
force-pushed
the
expriments/idris
branch
from
ff7112f to
d11c5d4
Compare
brendanzab
force-pushed
the
expriments/idris
branch
from
bf45ee3 to
5c175d4
Compare
brendanzab
force-pushed
the
expriments/idris
branch
from
5c175d4 to
1c37a1c
Compare
brendanzab
force-pushed
the
expriments/idris
branch
from
43c8e50 to
00b265b
Compare
brendanzab
force-pushed
the
expriments/idris
branch
from
00b265b to
bac5789
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Just a draft for now, but thought I’d publish if anyone was interested.
I was sketching some of this out in text files but thought it would be nice to share my thinking. Hopefully it helps in pondering some of the issues related to let formats and constrained representation types.