Folder Structure:

The repository is split into documents and the agda-playground folder. All the code and resources associtated with it are in the agda-playground folder.

agda-playground contains all the Agda code that I have written.

The main folder is fingertree.

  Here we find the files that are needed for the dissertation.

  FingerTree-Isabelle is the implementation of the FingerTree as presented on the
Isabelle page. I find it relevant as it shows how much easier proofs become when
we give up the nested structure, to the cost of explicitly mentioning level constraints.

  FingerTree-measure is the main implementation of the fingerTree, which is both
nested and contains the measurment information necessary for building further data structures on top

  FingerTree-Measured-Isabelle is a failed attempt of adding the measurement info to the
isabelle implementation

  FingerTree-Node1 is an attempt to make proofs easier by copying some of the isabelle ideas - it failed.

  FingerTree is the original implementation by the guy on github, modified to run and some explanations of
why proofs are hard.

  measure.agda is not used.

  numbers.agda provides lemmas about natural numbers and lists which are being used in the examples.

  There is also a Class folder, which comes from the Standard library but I added it here because I wanted to change something

  The NestedDatatypes folder gives some more examples of nested datatypes and proofs on them (nest and debrujin notation)

Another important file is a syntax_notes.txt where I am writing Agda knowledge that I find bizzare and easy to forget.

In the agda-playground, more important are chalmers which is the original tutorial and llrb which is an example of previous work done in this field.

The Agda version I am using is 2.5.1.1