Arthur Paulino

Sure, go for it 👍🏼

How are `nil` checks performed in the circuit? Is it done with some hardcoded value for the hash?

No, we're still using `ExprTag::Nil`

Since this also happens on the [Lean alternative implementation](https://github.com/lurk-lab/Lurk.lean/blob/0e6d48155863c4f4867a8381612f05cea09875b4/Lurk/New/Eval.lean#L270-L273), we believe that this is a limitation of the expected behavior rather than a real bug. So we should address this...

@jobez these can be the target for a first round: https://github.com/lurk-lab/lurk-rs/blob/6d0f79cafca953b8b39d72cf96cbb30a08d24612/src/lem/circuit.rs#L41-L43

Yes, this issue is specific to the Circom coprocessor itself, which wasn't changed when adapted to LEM

@tchataigner we mean the arguments we pass in a Lurk program like `foo` in `(sha256 foo)`

This was originally @gabriel-barrett's idea and is not implemented yet. So I defer the answer to him

Given that we have `eq`, would `type-eq` be a more consistent name? E.g. `(type-eq 0 0)`

What kind of bugs me with this approach is that type-equality doesn't entail a particularly interesting semantic for two arbitrary inputs. So what's likely to happen with real Lurk code...