2017-05-09 4 views

答えて

5

このイドリスはpostを郵送することを示唆したよう:分で

、名前アクセスできないになります(まだ文書化されていないなど)%hideディレクティブは、すべてそこにあります。ここで

例です。

%hide fib 

fib : Nat -> Nat 
fib Z = Z 
fib (S Z) = S Z 
fib (S (S n)) = fib n + fib (S n) 
+0

感謝。 %hideが行うことに関する文書はありますか? –

+0

いいえ、実際はありません。この[構文ガイド](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)。 –

+0

構文ガイドはそれほど役に立ちません。私が推測したのは、エクスポートしていたものを隠していたのですが、インポートしていませんでした。 –

関連する問題