Extracted property-based testing machinery into its own module.

1 files changed, 51 insertions, 47 deletions

diff --git a/documentation/bookmark/type_theory/dependent.md b/documentation/bookmark/type_theory/dependent.md
index f731e988a..03a5606ec 100644
--- a/documentation/bookmark/type_theory/dependent.md
+++ b/documentation/bookmark/type_theory/dependent.md
@@ -1,56 +1,60 @@
 # Exemplar
 
-1. [Mononym: Type-Level Named Values in Rust - Part 1: Demo and Implementation](https://maybevoid.com/blog/mononym-part-1/)
-1. [POMPOM LANGUAGE](https://github.com/caotic123/PomPom-Language)
-1. [A simple type-theoretic language:  Mini-TT](http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf)
-1. https://cedille.github.io/
+0. []()
+0. [Mononym: Type-Level Named Values in Rust - Part 1: Demo and Implementation](https://maybevoid.com/blog/mononym-part-1/)
+0. [POMPOM LANGUAGE](https://github.com/caotic123/PomPom-Language)
+0. [A simple type-theoretic language:  Mini-TT](http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf)
+0. https://cedille.github.io/
 
 # Reference
 
-1. [A Language Agnostic Introduction to Dependent Types](https://www.shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html)
-1. [The Gentle Art of Levitation](http://lambda-the-ultimate.org/node/5526)
-1. [Programming up to Congruence](http://www.cs.yale.edu/homes/vilhelm/papers/popl15congruence.pdf)
-1. [From Scheme to Dependent Types in 100 lines by Gershom Bazerman (Part 1)](https://vimeo.com/134561872)
-1. [From Scheme to Dependent Types in 100 Lines by Gershom Bazerman (Part 2)](https://vimeo.com/135746080)
-1. [Program = Proof](http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf)
-1. [Multimodal Dependent Type Theory](https://arxiv.org/abs/2011.15021)
-1. [Thorsten Altenkirch - The power of Π - Lambda Days 2020](https://www.youtube.com/watch?v=3zT5eVHpQwA)
-1. [A Path To DOT: Formalizing Fully Path-Dependent Types](https://arxiv.org/abs/1904.07298)
-1. [Ghosts of Departed Proofs (Functional Pearl)](https://www.youtube.com/watch?v=2cAxOJEiL00)
-1. [Ghosts of Departed Proofs (Functional Pearl)](https://kataskeue.com/gdp.pdf)
-1. [F# Linear algebra with type-level dimensions and static checks](https://notebooks.azure.com/allisterb/projects/sylvester/html/Sylvester.Tensors.ipynb)
-1. [From Scheme to Dependent Types in 100 lines by Gershom Bazerman](https://vimeo.com/134561872 &&& https://vimeo.com/135746080)
-1. [A Tutorial Implementation of a Dependently Typed Lambda Calculus](https://www.andres-loeh.de/LambdaPi/)
-1. [The calculus of constructions](http://www.sciencedirect.com/science/article/pii/0890540188900053#)
-1. https://www.idris-lang.org/
-1. https://www.amazon.com/Type-driven-Development-Idris-Edwin-Brady/dp/1617293024/
-1. http://blog.codersbase.com/posts/2013-12-03-learning-dependent-types.html
-1. http://oxij.org/note/BrutalDepTypes/
-1. https://hydraz.club/posts/2017-09-08.html
-1. [Hoare Type Theory, Polymorphism and Separation](http://ynot.cs.harvard.edu/papers/jfpsep07.pdf)
-1. ["Dependent Types in Haskell" by Stephanie Weirich](https://www.youtube.com/watch?v=wNa3MMbhwS4)
-1. [A Little Bit of Dependent Types](https://youtu.be/WI8uA4KjQJk?t=5169)
-1. [Type Checking Without Types](https://matthias.benkard.de/typecore/typecore.pdf)
-1. [Cubical Type Theory: a constructive interpretation of the univalence axiom](http://www.cse.chalmers.se/~coquand/cubicaltt.pdf)
-1. https://github.com/mortberg/cubicaltt
-1. https://leanprover.github.io/introduction_to_lean/
-1. [Infinity](https://github.com/groupoid/infinity)
-1. https://github.com/groupoid
-1. http://groupoid.space/
-1. https://existentialtype.wordpress.com/2016/07/31/cubical-higher-type-theory-as-a-programming-language/
-1. https://github.com/silt-lang/silt
-1. [Parametric Quantifiers for Dependent Type Theory](https://people.cs.kuleuven.be/~andreas.nuyts/ParametricQuantifiers.pdf &&& https://www.youtube.com/watch?v=lJB5MhYJ4Js)
-1. [A Specification for Dependently-Typed Haskell:](http://www.seas.upenn.edu/~sweirich/papers/systemd-submission.pdf)
-1. [A Specification for Dependent Types in Haskell](http://www.seas.upenn.edu/~sweirich/papers/systemd-submission.pdf &&& https://cs.brynmawr.edu/~rae/papers/2017/dep-haskell-spec/dep-haskell-spec.pdf &&& https://www.youtube.com/watch?v=0157rUxC4_8)
-1. [Normalization by Evaluation for Sized Dependent Types](http://publications.lib.chalmers.se/records/fulltext/252072/local_252072.pdf &&& https://www.youtube.com/watch?v=uSP91COE_ZA)
-1. https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html
-1. [AN INTRODUCTION TO UNIVALENT FOUNDATIONS FOR MATHEMATICIANS](http://www.ams.org/journals/bull/2018-55-04/S0273-0979-2018-01616-9/S0273-0979-2018-01616-9.pdf)
-1. https://medium.com/@maiavictor/about-induction-on-the-calculus-of-constructions-581fcfdb89c5
-1. [05 A Dependent Haskell Triptych](https://www.youtube.com/watch?v=soKl1IslU-I)
-1. https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf
-1. [Algebraic Presentations of Dependent Type Theories](https://arxiv.org/abs/1602.08504v3)
+0. []()
+0. [Checking Dependent Types with Normalization by Evaluation: A Tutorial](https://davidchristiansen.dk/tutorials/nbe/)
+0. [A Language Agnostic Introduction to Dependent Types](https://www.shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html)
+0. [The Gentle Art of Levitation](http://lambda-the-ultimate.org/node/5526)
+0. [Programming up to Congruence](http://www.cs.yale.edu/homes/vilhelm/papers/popl15congruence.pdf)
+0. [From Scheme to Dependent Types in 100 lines by Gershom Bazerman (Part 1)](https://vimeo.com/134561872)
+0. [From Scheme to Dependent Types in 100 Lines by Gershom Bazerman (Part 2)](https://vimeo.com/135746080)
+0. [Program = Proof](http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf)
+0. [Multimodal Dependent Type Theory](https://arxiv.org/abs/2011.15021)
+0. [Thorsten Altenkirch - The power of Π - Lambda Days 2020](https://www.youtube.com/watch?v=3zT5eVHpQwA)
+0. [A Path To DOT: Formalizing Fully Path-Dependent Types](https://arxiv.org/abs/1904.07298)
+0. [Ghosts of Departed Proofs (Functional Pearl)](https://www.youtube.com/watch?v=2cAxOJEiL00)
+0. [Ghosts of Departed Proofs (Functional Pearl)](https://kataskeue.com/gdp.pdf)
+0. [F# Linear algebra with type-level dimensions and static checks](https://notebooks.azure.com/allisterb/projects/sylvester/html/Sylvester.Tensors.ipynb)
+0. [From Scheme to Dependent Types in 100 lines by Gershom Bazerman](https://vimeo.com/134561872 &&& https://vimeo.com/135746080)
+0. [A Tutorial Implementation of a Dependently Typed Lambda Calculus](https://www.andres-loeh.de/LambdaPi/)
+0. [The calculus of constructions](http://www.sciencedirect.com/science/article/pii/0890540188900053#)
+0. https://www.idris-lang.org/
+0. https://www.amazon.com/Type-driven-Development-Idris-Edwin-Brady/dp/1617293024/
+0. http://blog.codersbase.com/posts/2013-12-03-learning-dependent-types.html
+0. http://oxij.org/note/BrutalDepTypes/
+0. https://hydraz.club/posts/2017-09-08.html
+0. [Hoare Type Theory, Polymorphism and Separation](http://ynot.cs.harvard.edu/papers/jfpsep07.pdf)
+0. ["Dependent Types in Haskell" by Stephanie Weirich](https://www.youtube.com/watch?v=wNa3MMbhwS4)
+0. [A Little Bit of Dependent Types](https://youtu.be/WI8uA4KjQJk?t=5169)
+0. [Type Checking Without Types](https://matthias.benkard.de/typecore/typecore.pdf)
+0. [Cubical Type Theory: a constructive interpretation of the univalence axiom](http://www.cse.chalmers.se/~coquand/cubicaltt.pdf)
+0. https://github.com/mortberg/cubicaltt
+0. https://leanprover.github.io/introduction_to_lean/
+0. [Infinity](https://github.com/groupoid/infinity)
+0. https://github.com/groupoid
+0. http://groupoid.space/
+0. https://existentialtype.wordpress.com/2016/07/31/cubical-higher-type-theory-as-a-programming-language/
+0. https://github.com/silt-lang/silt
+0. [Parametric Quantifiers for Dependent Type Theory](https://people.cs.kuleuven.be/~andreas.nuyts/ParametricQuantifiers.pdf &&& https://www.youtube.com/watch?v=lJB5MhYJ4Js)
+0. [A Specification for Dependently-Typed Haskell:](http://www.seas.upenn.edu/~sweirich/papers/systemd-submission.pdf)
+0. [A Specification for Dependent Types in Haskell](http://www.seas.upenn.edu/~sweirich/papers/systemd-submission.pdf &&& https://cs.brynmawr.edu/~rae/papers/2017/dep-haskell-spec/dep-haskell-spec.pdf &&& https://www.youtube.com/watch?v=0157rUxC4_8)
+0. [Normalization by Evaluation for Sized Dependent Types](http://publications.lib.chalmers.se/records/fulltext/252072/local_252072.pdf &&& https://www.youtube.com/watch?v=uSP91COE_ZA)
+0. https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html
+0. [AN INTRODUCTION TO UNIVALENT FOUNDATIONS FOR MATHEMATICIANS](http://www.ams.org/journals/bull/2018-55-04/S0273-0979-2018-01616-9/S0273-0979-2018-01616-9.pdf)
+0. https://medium.com/@maiavictor/about-induction-on-the-calculus-of-constructions-581fcfdb89c5
+0. [05 A Dependent Haskell Triptych](https://www.youtube.com/watch?v=soKl1IslU-I)
+0. https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf
+0. [Algebraic Presentations of Dependent Type Theories](https://arxiv.org/abs/1602.08504v3)
 
 # Math | Proofs
 
-1. http://logipedia.inria.fr/about/about.php
+0. []()
+0. http://logipedia.inria.fr/about/about.php