Hiearchy builder in Lean

Stream: lean4

[Cyril Cohen]

Hi, I'd be interested in porting Hiearchy Builder to Lean4, with a hybrid TC + UH encoding if possible, if someone is working on it or interested in working on it please tell me.

[Cyril Cohen]

I must say that I will be pretty busy in the coming months, but this is mostly a declaration of interest.

[Cyril Cohen]

And to open the discussion

[Cyril Cohen]

Maybe it's worth posting our paper about HB here: https://hal.inria.fr/hal-02478907v5

[Ryan Lahfa]

Cyril Cohen said:

Hi, I'd be interested in porting Hiearchy Builder to Lean4, with a hybrid TC + UH encoding if possible, if someone is working on it or interested in working on it please tell me.

I thought of trying my hand of understanding HB (and implementing very simple prototype of it in Lean 4, but failed!) during this summer and was really interested into it. I'd be definitely interested into pushing some humble pull requests if there is any public repository :).

By the way, what is "UH encoding"? (advanced googling did not help, a lot, except suggesting something related to fibrant types.)

Thank you!

[Ryan Lahfa]

(ha, UH = universe hierarchy?)

[Alex J. Best]

Unification hints?

[Karl Palmskog]

https://link.springer.com/chapter/10.1007/978-3-642-03359-9_8 / http://www.cs.unibo.it/~asperti/PAPERS/tphol09.pdf ("Hints in unification", TPHOLs 09)