Nadrieril

Also this would give us a way to test any two values for equality. The idea is that since `Map/alter` only changes the entry at a given key, if we...

What does this mean for the value of the Map to be "immediate" ? Is that something straightforward to check during typechecking ?

@Gabriel439 I don't think I understand what you're saying. Typechecking toMap only checks that the type of its the argument is a record type. `\(x: { ... }) -> toMap...

Ok, if I understand correctly we would, at typechecking time, evaluate the argument of fromMap, and verify that it is a list literal containing records of the appropriate type, and...

Now that I think about it, I wouldn't mind if normalizing renamed variables to avoid shadowing. E.g. `λ(x : Natural) → let y = x in λ(x : Bool) →...

It would also help alleviate the problem of the alpha-normalization of cached imports since alpha-normalized values would be much more readable

If that's the issue, we could easily say this is a new syntax and parse `x_1` as `("x", 1)` internally. Ah, in fact we could reuse the `@` syntax. So...

I see a lot of enthusiasm ! @Gabriel439 May I ask you to do the basic setup of a Haskell project ? It's been a while since I've written any...

Well, my intentions are definitely about having as much as possible of the standard made executable. Hand-rolling and maintaining a parser is a huge effort, I'd rather avoid that :/...

Hey, sorry for letting this slip away. Life happened and I've sadly been cutting down on time invested in Dhall. This issue in particular is a huge undertaking that I...