#agdaで data List (A : Set) : Set whereとあるところで
#data List : (A : Set) -> Set whereというのはダメなのね。
#なんか型コンストラクタだという風に考えると
#こう書けてもよさそうなのになんか納得いかないんだけど、どういうことなんだろう
#あと、Vecとかも
#Vec (A : Set) : (n : Nat) -> Set where
#は
#data Vec : (A : Set) -> (n : Nat) -> Set where
#とかダメなのだけどAとnで扱いが違うのナットクいかん。
#さらにVecのコンストラクタで_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
#のところでinplicit argの{n : Nat}が必要っぽいんだけどなんで？
#data宣言の部分に登場しているのは関係ないの？
#このあたりがどのチュートリアルも天下り式に書いてあって、きちんとしたルールが見えないので応用がきかない。というか自分で書くとtry&errorになってストレスにしかならん。誰か分かりやすくおねがい!!
#Agda のはなし、ここでするのは off-topic な感ありますが
#ま、そうなんですけどね。
#それはさておき、寝て起きてから、なにか教えます
#わぁ、ありがとうございます!
#私も寝ますゆえ。
#教科書的な答を言うと、Agda mailing list に投げれば素早く帰ります
#notogawa さんは、ここ見てたら、何を読んでそこまで理解できたか、皆さんと共有してください…
#ぼくは nethack の不思議を知るのにソースコードを grep するのが好きなので、これはとうていお勧めできない
#Haskell の話なんですよということを言うと、Agda の構文木は src/full/Agda/Syntax/Abstract.hs の data Expr (snip) にあるので、起点はここです
#最後の部分に関しては、Agda のデータ型は基本的に Haskell でいう GADTs で、GADTs は型引数の形をコンストラクタで制御出来るようなデータ型なので、一般に宣言部の型と、データ構築子で導入する型が一致していたら嬉しさがないですよね。
#？？？具体例を出せますでしょうか
#それはともかく、最初の質問の List なり Vec なりの : の前後、なにがちゃうねんというのは
##がよいと思います（他にもあればご指導ください）
#ん、ああ、すいません、ちょっと勘違いしてました
#: の左側は型パラメタとして定義全体で共有されるけど、右側は後で受け取られるパラメタなわけですね
#たとえば、上の Vec の定義の頭の部分は
#data Vector (A : Set) : Nat → Set where
#と書いても問題がないのです。 Nat が何かは後で決まるから
#で、その Nat が何かを知るために、implicit parameter が必要になる……というのは駄目でしょうか
#かならずしも必要ではない、というのが状況に混乱をもたらします
##たとえば、こうも書けます
#すいません、ちょうど今僕もAgda書いているんですが、このNatのNはagda-modeでどうやって入力すればいいのでしょうか。チートシートが欲しい。。
#横道にそれますが、 chaton さんの文字コードなんだろう charset の宣言が見当たらないのでブラウザのデフォルト？
#Nat の N は agda-mode が利用している agda-input で \bn です
#ありがとうございます！
#KANJI FEP ぽい
#Agda Wiki上から辿れるpaperと標準ライブラリが情報源ですが，私は後者を眺めてる比率が大きいです．
##notogawa さんの Q にたいする DecTotalOrder みんな幸せになりそうですが、公式にマージしませんか（お給料でませんが…
#あ，元々パッチ投げるつもりで書いてて
#今ちょっとリファクタリングしてるとこです．
#土日くらいには仕上げるハラヅモリで
#ikegami__: ありがとうございます。\toとかも知らずにATOKで変換してました。
#\-> とか形状から類推しても入れられますよね。\--> とするとほんの僅かだけちょっと長い矢印が入力されたり（群準同型をあらわすのに -Group⟶ とか使ってたりする）
#おおすごい。これは便利だ。
#Thierry 先生に『日本語どうやって入力するの？』って聞かれて教えた記憶があるのですが、その後 Agda2 に実装されていて大変おどろきました（Emacs の達人がワザを見せたようだ
#IRC の freenode #agda も英語で質疑応答がなされており、それなりに active な様子です（僕は join してません
##Agda の live coding を見つけました。 {n : Nat} を付け忘れて困ったのでやりなおし(11分あたり) とか見れます。そのままでは小さくて見えないので、右下にある拡大ボタンを適宜押してください : #URL 書いたら、ここにでてくるんだ…
#動画良さそうです。ありがとうございます。
#さかいさんも昔同じようなムービーを作っていた記憶があります
#パラメータとインデクスの差ですか。パラメータはコンストラクタの宣言部でも同じものが見えるのですか。
#入力に関しては私はagda-modeのagda-input.elを見て覚えたりしてます。まだちょくちょく確認しないと…だけど、よく使うものはなれてきました。¥bnとか¥->や¥(¥)とかのカッコ系くらいですけど。
#パラメタとインデクスはUlfのチュートで順に説明されてたけど、型か値かの違いくらいに思ってていいのかな。
#¥lambda¥_2¥^2¥allあたりも使うか。
haskell-ja > Archives > 2013/04/11