ロケールでの型変数の制限

Isabelleライブラリには、real_innerとreal_normed_vectorというクラスがあり、後者は前者のサブクラスである~~src/HOL/Library/Inner_Product.thyと宣言されています。今ロケールでの型変数の制限

、我々はロケール

locale foo = 
    fixes goo :: "'a::{real_normed_vector} => bool"

といくつかの新しい定数と、このロケールを拡張したいを持っており、またそのように、同時にreal_innerする'aの並べ替えを拘束したとします

locale extended = foo + 
    fixes ext :: "'a::{real_inner} => nat"

これを行う方法はありますか？上記の例を使用してこれを実行しようとすると、'b::{real_normed_vector} => boolのextendedにIsabelleがgooというタイプを指定していますが、代わりにタイプ'a::{real_inner} => boolが必要です。

あなたはこのようにそれを行うことができます。

locale extended = foo goo 
    for goo :: "'a :: real_inner ⇒ bool" + 
    fixes ext :: "'a => nat"

2017-01-06 15:08:27

感謝。私は質問をする前にこれを試しましたが、何がうまくいかないのかを偽った別の問題がありました。今は固定されています。 –

答えて