問題タブ [agda]

A foreword note that this is for an assignment. A question has already been asked about for the first question. So we have the data type:

Now we're being asked to write the proposition

which should return BoolProp false

I'm Just getting confused on how to do this. Ptrue returns BoolProp true however with the data type por takes in two Bool's not BoolProp's. Maybe the data type is wrong. Any heads up would be great

I should add that the eval code is a snippet from the haskell code

note: editted it to not give everything away

注意点として、これは課題のためのものであるため、完全な解決策を投稿しないのがおそらく最善です。むしろ、私は立ち往生していて、次に何を見るべきかについていくつかのヒントが必要です。

これらはすでにインポートされています：

BSTの範囲を広げるこの関数を実装する必要があります。

私はこれまでにこれを持っています：

新しい境界は厳密に最小/最大よりも小さい/大きい必要がないため、これは明らかに機能しません。ヒントが与えられました。It is not strictly necessary, but you may find it helpful to implement an auxiliary function that widens the range of a strictly smaller than relation of the form min < max.これは私がここで行ったことの一種であり、明らかにいくつかの変更が必要ですが、基本的な考え方はそこにあると思います。

これが私が今いるところです、そして私はここからどこへ行くべきかについて本当に行き詰まっています、私はできる限り多くの研究をしました、しかしAgdaを使うためにそこにたくさんの読み物がありません。おそらく≤-reflまたは≤-transを使用する必要がありますか？

Agda は、依存型を調査し、直観主義型理論をいじり、これらの実装を試すのに適したプログラミング言語です。しかし、Agda で書かれた「実際の」プログラムの例は既にあるのでしょうか? その機能を誇示する例もあるかもしれません (「実際の」Haskell プログラムの例として xmonad がよく言及されるのと同様です)?

私は最近、Haskell と Agda (従属型関数型プログラミング言語) を取り上げた大学のコースを修了しましたが、これらのラムダ計算を組み合わせロジックに置き換えることができるかどうか疑問に思っていました。Haskell では、これは S および K コンビネータを使用して可能であるように思われるため、ポイントフリーになります。アグダに相当するものは何だろうと思っていました。つまり、依存型の関数型プログラミング言語を、変数を使用せずに Agda と同等のものにすることはできますか?

また、どうにかして定量化をコンビネータに置き換えることは可能ですか? これが偶然かどうかはわかりませんが、たとえば全称量化により、型シグネチャがラムダ式のように見えます。意味を変えずに型シグネチャから全称量化を削除する方法はありますか? 例:

forallを使わずに同じことを表現できますか？

「checkSimple」は、ユニバースUの要素であるuを取得し、（nat 1）がuで指定されたagdaタイプに変換できるかどうかをチェックします。変換の結果が返されます。

次に、コンソールプログラムを作成して、コマンドラインから「someU」を取得しようとしています。

そのため、「checkSimple」のタイプを変更して、パラメーターとして（u：たぶんU）を含めました（たぶん、コンソールからの入力は「nothing」である可能性があるため）。ただし、タイプチェックするコードを取得できません。

Agdaでネストされたリストを解析しようとしています。私はグーグルで検索し、私が見つけた最も近いものはHaskellでアドレス指定された解析ですが、通常、Agdaでは利用できない「parsec」のようなライブラリが使用されます。

"((1,2,3),(4,5,6))"したがって、結果タイプを。で解析したいと思い(List (List Nat))ます。

さらにネストされたリストをサポートする必要があります（深さ5まで）。たとえば、深さ3はです(List (List (List Nat)))。

私のコードは非常に長くて面倒で、(List (List Nat))ネストされたリストに対してのみ機能しますが、機能しません。私は自分で進歩を遂げませんでした。

役に立ったら、以前の投稿の最初の回答splitByから再利用したいと思います。

EDIT1 **

ICFPでのコナーの講演はオンラインです-タイトルは「Agda-curious？」です。
2日前からです。見てみな！！
。
ビデオを見る：
http ：//www.youtube.com/watch？v = XGyJ519RY6Y

--EDIT2
：
解析に必要なコードに近いと思われるリンクを見つけました。提供される関数
があります： https ：//github.com/fkettelhoit/agda-prelude/blob/master/Examples/PrefixCalculator.agdatokenize

--EDIT3
：
私はついに十分に高速なはずの単純なコンビネータライブラリを見つけました。ライブラリには例が含まれていないので、問題を解決する方法を探す必要があります。
リンクは次のとおりです。

https://github.com/crypto-agda/agda-nplib/blob/master/lib/Text/Parser.agda

オンラインでNicolasPouillardからのagdaコードがもっとあります：
https ：//github.com/crypto-agda

最初のいくつかの退屈なインポート:

ここで、たとえば Naturals によって索引付けされた型があるとします。

そして、この型で動作する関数についていくつかの等式を証明したいと思いFooます。agda はあまりスマートではないため、これらは異種の等式になります。簡単な例は次のとおりです。

バーでの目標は

これら|はゴールで何をしていますか？そして、どうすればこのタイプの用語を構築し始めることができるでしょうか?

この場合、手動で を使用して置換を行うことで問題を回避できますがsubst、大きな型や方程式の場合、これは非常に見苦しく退屈になります。

Agdaでは、aのタイプはforall、次のすべてがタイプを持つように決定されますSet1（ここSet1で、はタイプであり、タイプSetはAタイプですSet）。

ただし、次のタイプは次のとおりSetです。

タイプがあった場合、矛盾が生じることは理解してSetいSetますが、上記の3つの用語のいずれかにタイプがあった場合、どのように矛盾が生じるかはわかりませSetん。それらを使用してFalseを証明できますか？それらを使用してそれを示すことができますSet : Setか？