idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-28 22:22:10 +03:00
Code Issues Projects Releases Wiki Activity

Add DOI to Liam's search paper stuff

Browse Source
This commit is contained in:
Thomas E. Hansen 2022-08-31 15:41:48 +02:00 committed by CodingCellist
parent 23eea52c50
commit a90fe03ff7
3 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libs/papers/Search/Generator.idr
View File

@ -1,6 +1,7 @@
||| The content of this module is based on the paper
||| Applications of Applicative Proof Search
||| by Liam O'Connor
||| https://doi.org/10.1145/2976022.2976030
|||
||| The main difference is that we use `Colist1` for the type of
||| generators rather than `Stream`. This allows us to avoid generating

1
libs/papers/Search/HDecidable.idr
View File

@ -1,6 +1,7 @@
||| The content of this module is based on the paper
||| Applications of Applicative Proof Search
||| by Liam O'Connor
||| https://doi.org/10.1145/2976022.2976030
module Search.HDecidable

1
libs/papers/Search/Properties.idr
View File

@ -1,6 +1,7 @@
||| The content of this module is based on the paper
||| Applications of Applicative Proof Search
||| by Liam O'Connor
||| https://doi.org/10.1145/2976022.2976030
module Search.Properties