"checkSimple" 获取 u，Universe U 的一个元素，并检查 (nat 1) 是否可以转换为给定 u 的 agda 类型。返回转换的结果。
现在我尝试编写一个控制台程序并从命令行获取“someU”。
因此，我将“checkSimple”的类型更改为包含一个 (u: Maybe U) 作为参数（可能是因为来自控制台的输入可能是“无”）。但是我无法获取代码进行类型检查。
module CheckMain where
open import Prelude
-- Install Prelude
---- clone this git repo:
---- https://github.com/fkettelhoit/agda-prelude
-- Configure Prelude
--- press Meta/Alt and the letter X together
--- type "customize-group" (i.e. in the mini buffer)
--- type "agda2"
--- expand the Entry "Agda2 Include Dirs:"
--- add the directory
data S : Set where
nat : (n : ℕ) → S
nil : S
sToℕ : S → Maybe ℕ
sToℕ (nat n) = just n
sToℕ _ = nothing
data U : Set where
nat : U
El : U → Set
El nat = ℕ
sToStat : (u : U) → S → Maybe (El u)
sToStat nat s = sToℕ s
-- Basic Test
test1 : Maybe ℕ
test1 = sToStat nat (nat 1)
{- THIS WORKS -}
checkSimple : (u : U) → Maybe (El u)
checkSimple someU = sToStat someU (nat 1)
{- HERE IS THE ERROR -}
-- in contrast to checkSimple we only get a (Maybe U) as a parameter
-- (e.g. from console input)
check : {u : U} (u1 : Maybe U) → Maybe (El u)
check (just someU) = sToStat someU (nat 1)
check _ = nothing
{- HER IS THE ERROR MESSAGE -}
{-
someU != .u of type U
when checking that the expression sToStat someU (nat 1) has type
Maybe (El .u)
-}