Karl Meakin
Karl Meakin
> One nit-pick: could we use the actual the actual type names rather than `Self` in impls and type definitions etc? I prefer to only use those when necessary in...
I would recommend against using integer IDs instead of pointers: * Have to pass the arena to any code that wants to dereference an ID * `fmt::Debug` output is less...
# The cause * Generate a fresh meta variable for the result of the match term * Push a local parameter for the placeholder pattern * Check `0 + 0`...
Removed implicit extension because it could silently change the result of expressions (eg `(u16_extend_u64 x * u16_extend_u64 y) != u16_extend_u64 (x * y)`)
> The resulting terms are a bit larger than I’d like, because we need to quote type annotations back to terms during elaboration. Glued evaluation potentially help here. Should be...
> Does having explicit type annotations help you in something you are looking at? Should we try to get this merged? No, I just wanted symmetry with the type annotations...
> Oh wow, neat. Do you have any ideas about how this might interact with termination checking? IIUC some type theories have a type for “well founded recursion”, but this...
> I do also wonder also if it would be better (in Fathom) to limit recursive bindings to the top level. I decided to do local recursive binding first, because...
> Very nice, I’m happy with this. Is there anything else that needs to be done to the before merging? I would like to still use eager evaluation for "runtime"...
Should types of items/metavars/local vars be lazily evaluated too?