Adrien Champion

@Kha I would be interested in giving this a try. As discussed on Zulip, it seems relatively reasonable for my first issue. I'll start looking into it but I'll take...

Once you have a `HConsed` value, you can weak-ify it using [`to_weak`](https://docs.rs/hashconsing/1.5.1/hashconsing/struct.HConsed.html#method.to_weak).

I took a brief look at `weak_table`, and it seems to be compatible with them we need to implement some trait, probably [`WeakElement`](https://docs.rs/weak-table/latest/weak_table/traits/trait.WeakElement.html), and/or give access to `Weak` ref stored...

I prefer the latter as it avoids conditionally depending on yet another library, what do you think @vleni ?

Hi @asvarga! Sorry for the delay. I'm not sure how this is intended to be used as I don't use `weak_table` myself, it was a feature request. However, looking at...

@asvarga @vleni I created #19 to get a sense of the interest in actual `weak_table` integration, which would be much nicer for you guys

Sounds good, I'll merge that ASAP, thank you for your feedback 😺

I'm not sure I understand how rsmt2 fits here. rsmt2 requires your solver to support (some slight variations of) SMT-LIB 2, in an *interactive* manner on stdin / stdout. In...

No worries. So yeah, if you want rsmt2 to be able to use your solver you need to be able to read SMT-LIB 2 from your standard input *interactively*, and...

Solved simp-normal form issues, but I'm not sure what to do with ```lean @[simp 1100] theorem modifyHead_modifyHead (l : List α) (f g : α → α) : (l.modifyHead f).modifyHead...