this repo has no description www.jonmsterling.com/01HC/
dependent-types proof-assistant swift

Refactor the value/neutral representation #2

open opened by jonmsterling.com

Right now, value frames get "enriched" to include type information when they are applied to a neutral. There is a lot of thunking going on and this is making things kind of complicated. Ideally this wouldn't be needed at all.

I would like to move to something closer to https://github.com/AndrasKovacs/2ltt-impl/blob/main/src/Core/Value.hs. This change would touch a huge amount of code, which makes me think it is better to do it now than later.

sign up or login to add to the discussion
Labels

None yet.

assignee

None yet.

Participants 1
AT URI
at://did:plc:jjiv56ot7d6sgethto3jr3r5/sh.tangled.repo.issue/3mhsc47alcw22