如何在Isabelle中定义子类型及其含义? [英] How to define Subtypes in Isabelle and what they mean?

问题描述

关于Isabelle中的子类型的问题非常冗长

The question regarding subtyping in Isabelle is very lengthy here. So my simple question is that how I can define type B to be a subtype of A if I define A as below:

typedecl A

这样做，我想使类型B的元素可以访问在A上定义的所有操作和关系(此处未打印).

By doing this I would like to make all operations and relations defined over A (they are not printed here) accessible to elements of type B.

一个更复杂的示例是将B和C定义为A的子类型，以使B和C不相交，并且A的每个元素都是B类型或C类型.

A bit more complex example is to define B and C to be subtype of A such that B and C are disjoint, and every element of A is either of type B or of type C.

谢谢

推荐答案

Isabelle没有子类型，尽管子类型的某些方面可以如所解释的那样进行仿真

Isabelle does not have subtypes, although some aspects of subtyping can be emulated as explained in another thread. If you want to use the same operation on different types, you may want to look into Isabelle's type classes.

这篇关于如何在Isabelle中定义子类型及其含义?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！