在命令行中输入 idris 来启动交互式环境。你会看到如下内容： $ idris ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 1.3.1 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help Idris> 以提升未来的加载速度。在源文件被修改之后，字节码会 重新生成。 $ idris hello.idr ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 1.3.1 _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help Type 描述 述 述 包的描述包含以下内容： • 包头，由关键字 package 后跟一个包名构成。包名可以是任何有效的 奉 奤 奲 奩 女 标识符。 奩 奐 奋 奇 格式 也可包含一个带引号的 version，它接受任何有效的文件名。 • 描述包内容的字段， = 其中至少有一个 奭 奯奤 奵 奬 奥 女 字段，对应的值为逗号分隔的模块列表。例如， 给定一个 奉 奤 奲