Recognize Fin instances as nat literals too?

[ice1000]

@imkiva any ideae?

[imkiva]

Actually there's a Fin shape from the very beginning, but I gave up when I need to create a Nat where a representation of Fin is needed. But I am not sure if it becomes simpler with MetaLit now. Will give it a try.

[ice1000]

@imkiva You just have to generate fsuc a instead of suc a, but this has to be a concrete syntax.

[HoshinoTented]

One possible problem is type inferring, we won't infer 114514 : {?} to 114514 : Fin 0.
Inferring a meta Fin (114514 + {?}) would be a big challenge.

[ice1000]

lmao yeah

[ice1000]

We should do index erasure in an IR and run the shape matcher again. Vec will be matched with List and Fin/∈ will be matched with Nat.