5
fib
の自分のバージョンを再生したいのですが、fib
はPrelude
でエクスポートされます。 Prelude
からインポートを非表示にするにはどうすればよいですか?ハスケルでは、私はimport Prelude hiding (fib)
と書くだろうが、Idrisではうまくいきません。Idrisでは、Preludeで定義されているものをどのように隠すのですか?
fib
の自分のバージョンを再生したいのですが、fib
はPrelude
でエクスポートされます。 Prelude
からインポートを非表示にするにはどうすればよいですか?ハスケルでは、私はimport Prelude hiding (fib)
と書くだろうが、Idrisではうまくいきません。Idrisでは、Preludeで定義されているものをどのように隠すのですか?
このイドリスはpostを郵送することを示唆したよう:分で
、名前アクセスできないになります(まだ文書化されていないなど)
%hide
ディレクティブは、すべてそこにあります。ここで
例です。
%hide fib
fib : Nat -> Nat
fib Z = Z
fib (S Z) = S Z
fib (S (S n)) = fib n + fib (S n)
感謝。 %hideが行うことに関する文書はありますか? –
いいえ、実際はありません。この[構文ガイド](https://github.com/idris-lang/Idris-dev/blob/fb9a5ec0080020b5289a95658920ab9524be39b0/docs/reference/syntax-guide.rst#L470)とこの[メーリングリストの投稿](https: //groups.google.com/d/msg/idris-lang/fRQxu6EuUgM/nuWQmjL-svAJ)。 –
構文ガイドはそれほど役に立ちません。私が推測したのは、エクスポートしていたものを隠していたのですが、インポートしていませんでした。 –