idrisIdris> :t the
the: (a: Type) -> a -> a intId = the Nat とすれば、 intId はNat専用の恒等関数になるidrintId = the Nat
intId 3 -- 3
intId "hoge" -- error the 型 値 と書いて「その型は、その値を許容するか」を確認できる Fin は一つの自然数型をとって、それ未満の自然数を許容する型になるが、それを確認してみるidrthe (Fin 3) 3 -- error
the (Fin 3) 2 -- FS (FS FZ)