Skip to content

jpcooper-zz/agda-gp

 
 

Repository files navigation

attempts:

- tried to give a spine representation of spine, but later realised that sum is
  achieved by a list of Sigs in spine.
- attempting to convert a [Sig] into LIGD representation. Possibly generating the EP.
- defining spine and ligd in agda. not very interesting, but something time was spent on.

- spine == sum of products, except for existential types. 
- by converting to regular / ligd you lose information, since spine keeps track of the constructors



TODO:

- write about ligd and spine: comparison / similarities and possible translation
- why is spine supposedly bigger than ligd?

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published