Hopefully it is all a bit more precise now. Maybe someone wants to
formalize pattern.ML + unify.ML after > 20 years, to pin down the
remaining uncertaincies about type instantiation within these
non-trivial algorithms.
Just for the record, I would be interested in joining such an endeavor.
Unfortunately I'm not a proven expert ;)
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
