Email Gateway (Aug 22 2022 at 17:03): Email Gateway (Aug 22 2022 at 17:03):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Hi,
what papers should I read to understand the implementation of inductive
definitions in Isabelle?
Does this have anything to do with the new (co)datatype implementation?
Email Gateway (Aug 22 2022 at 17:04):From: Lawrence Paulson <lp15@cam.ac.uk>
I don't recall that anybody has answered this question. But I wonder what level of knowledge you want to have. Maybe it's enough if you read the following early paper:
http://www.cl.cam.ac.uk/~lp15/papers/Formath/milner-ind-defs.pdf
That's in the setting of set theory, so it is untyped and simple. Working with types adds some complications, and if you want to include recursive datatypes, it gets a lot more complicated still.
Larry
Last updated: Apr 18 2024 at 20:16 UTC