R2: I personally would be interested in dealing with the correspondence between trees and terms easily (in CoLoR for Coq terms are implemented using dependent types (number of arguments equal to the arity of the symbol); in Isafor for Isabelle they are implemented as rose trees (formally: using varyadic symbols), but i failed to make that work: (Error: Anomaly "Uncaught exception Failure("this kind of change is not yet supported")." Please report at http://coq.inria.fr/bugs/.) Will that be covered by future work?
It's kind of hard to know what R2 wants without seeing the type examples explicitly, but I should look into this at some point.
Also, I fixed this to not be an anomaly already, and to tell people to post issues here so I can ask them for their types.
tlringer
commented
4 years ago
R2: I personally would be interested in dealing with the correspondence between trees and terms easily (in CoLoR for Coq terms are implemented using dependent types (number of arguments equal to the arity of the symbol); in Isafor for Isabelle they are implemented as rose trees (formally: using varyadic symbols), but i failed to make that work: (Error: Anomaly "Uncaught exception Failure("this kind of change is not yet supported")." Please report at http://coq.inria.fr/bugs/.) Will that be covered by future work?
It's kind of hard to know what R2 wants without seeing the type examples explicitly, but I should look into this at some point.
Also, I fixed this to not be an anomaly already, and to tell people to post issues here so I can ask them for their types.