Agda の getArgs

五次の交換子を計算すると終わらないってのに気がついたんですが、

　　なんと、Agda から Haskell にコンパイルすると瞬時に終わる

それだと計算結果を証明に使えないのだが... まぁ、いろいろあるな。

で、そうすると、引数渡したくなるわけですが、

　　postulate
　　　 getArgs : IO (List String)
　　{-# FOREIGN GHC import qualified System.Environment　　#-}
　　{-# COMPILE GHC getArgs = System.Environment.getArgs #-}

とかしろとあるわけですが、まったく動かないです。IO coString だったりとか、getArgs が Data.Text.Text になったりで
おいていかれているっぽい。github 上の getArgsの例題が軒並み動かない。

まぁ、コンパイルするような言語じゃないからなぁ。