Skip to content
Commits on May 18, 2010
  1. Ignoring .vo files.

    committed
Commits on May 11, 2010
  1. @Eelis

    Add .gitignore.

    Eelis committed with
Commits on Apr 13, 2010
  1. Transcribing the content of [square_abstraction.v] to [hypercube_abst…

    Adam.Koprowski committed with
    …raction.v]... pretty mechanical work... maybe I should do some more thinking/planning?...
    
    darcs-hash:20100317170346-20b81-bd42d2e44196b1033a374b8c895075ee55388865.gz
  2. Simplified interface in [hypercube_abstraction.v]

    Adam.Koprowski committed with
    darcs-hash:20100317160907-20b81-5fa8d53592210f33d0e2b3c18dd57859863b754d.gz
  3. Defined [square] in [hypercube_abstraction.v]

    Adam.Koprowski committed with
    darcs-hash:20100317152418-20b81-ee63fc5f1bb18f34671b69dd4a5f9d48329e72aa.gz
  4. Defined the space in hypercube_abstraction.v

    Adam.Koprowski committed with
    darcs-hash:20100309150211-20b81-185632da21f0f891730b9155aee8ec5f40374b37.gz
  5. Switching to hlist_aux in abstract to define n-dimensional space; alm…

    Adam.Koprowski committed with
    …ost done but for a few wrinkles in hlist_aux.v
    
    darcs-hash:20100307132516-20b81-8d469bf46a8bb0649a45db9d0b24e68587043ee1.gz
  6. n-dimensional space defined anew (this time no universe inconsistency…

    Adam.Koprowski committed with
    … problems) but for a number of lemmas on a new variant of hlists.
    
    darcs-hash:20100228204829-20b81-ce854ddb59a1e254b7270e02efc5c2cd6a94ff41.gz
  7. Experimenting with different definitions of hlists (in hlist_aux.v) t…

    Adam.Koprowski committed with
    …o avoid universe inconsistency.
    
    darcs-hash:20100227121212-20b81-01f0a9812ceb6cb8b8284d5c934ee24f1252cd97.gz
  8. Finished defining n-dimensional space except for hitting Universe inc…

    Adam.Koprowski committed with
    …onsistency problem...
    
    darcs-hash:20100223162816-20b81-4a74f46d87ea6dd3c3ed1f6a2f34d3b8773576c9.gz
  9. Introducing monadic notation for DN and using it in one of the existi…

    Adam.Koprowski committed with
    …ng proofs to improve readability.
    
    darcs-hash:20100223161235-20b81-c132069a53fe65cf8ca16ea190cb0255e3218fb9.gz
  10. hyper_space (2D space generalized to n dimensions) defined except for…

    Adam.Koprowski committed with
    … the proof that regions cover invariants.
    
    darcs-hash:20100223152057-20b81-e38161ed621d7691f5ed6da83b3bbf082fa7250b.gz
  11. Finished proof of NoDup ExhaustiveHList.

    Adam.Koprowski committed with
    darcs-hash:20100222174144-20b81-42bada939c65d6f07807b00e9a89ef9f49216c72.gz
  12. Substantial progress in proving NoDup for ExhaustiveHList... but now …

    Adam.Koprowski committed with
    …time to board a plain... and sign off for the weekend... over
    
    darcs-hash:20100219214842-20b81-fd50f21c0aa5ebde00af5d6948b6419fb98fee08.gz
  13. Proven ExhaustiveList instance for hlist's

    Adam.Koprowski committed with
    darcs-hash:20100219171325-20b81-1c99791bdb47755bbd5daec48473ef8d7f9ea2fd.gz
  14. hlist.v: restructuring + small adjustements

    Adam.Koprowski committed with
    darcs-hash:20100219125431-20b81-35135a310b1710505bf2810ffd58ec3cba5d321c.gz
  15. hlist_prod_tuple adjusted for the purpose of instantiating Exhaustive…

    Adam.Koprowski committed with
    …List class for hlists.
    
    darcs-hash:20100219114355-20b81-b56a2bbc4a39d744c047a4817f03db268ff7888a.gz
  16. Finishing definition of hlist_prod_tuple for computing all combinatio…

    Adam.Koprowski committed with
    …ns of elements from a list of lists, thanks to A. Chlipala's help on the Coq's mailing list.
    
    darcs-hash:20100218212319-20b81-c7d6db09dbecb885c797216fc4c41ccc031499ce.gz
  17. A number of definitions on hlists.

    Adam.Koprowski committed with
    Almost defined a hlist_prod_tuple function that takes a hlist of lists and returns a list containing all the combinations of elements from all the lists. It will be used to provide an enumeration of all elements of hlists, given enumerations of all its types. But for now I hit some technical problems with recognizing that the principal argument is decreasing along recursive calls.... Duh, I do hate vim...................
    
    darcs-hash:20100218161505-20b81-27860d588b75a550f28f2063be3501e719d598e3.gz
  18. A set-up for providing n-dimensional space (as a generalization to pr…

    Adam.Koprowski committed with
    …oduct space)
    
    darcs-hash:20100217190334-20b81-1d839cf0775af2e0d09e77f4dbe4141540647b74.gz
  19. Decidability of equality for heterogenous lists proven with a Chlipal…

    Adam.Koprowski committed with
    …a-style proof... actually I start to buy into his "philosophy"
    
    darcs-hash:20100217182458-20b81-4aa7bda2b78de9750a30e207adb460babf2aabd4.gz
  20. Proven decidability of equality for heterogenous lists (but for two a…

    Adam.Koprowski committed with
    …uxiliary lemmas).
    
    darcs-hash:20100217143454-20b81-5842a6418e9e9a64cf8eca649a348a094eaa4e93.gz
  21. Added definition of heterogenous lists + hget function to get n'th el…

    Adam.Koprowski committed with
    …ement of such a list
    
    darcs-hash:20100217103841-20b81-ada2e20b34e8b81d69b69587ac5cb24f25d81f4b.gz
  22. Starting work on hyper-cube abstraction (generalizing square abstract…

    Adam.Koprowski committed with
    …ion to n-dimensional spaces)
    
    darcs-hash:20100216165612-20b81-03ed9905e12768b7d9e905220b200d38f896dcfe.gz
  23. coqc location taken from COQTOP environmental variable

    Adam.Koprowski committed with
    darcs-hash:20100216164636-20b81-5193467611b6ce3d48312026e17f13c755751be7.gz
Commits on Apr 8, 2010
  1. final ? updates

    Herman Geuvers committed
Commits on Apr 1, 2010
  1. @Eelis
Commits on Mar 30, 2010
  1. Adapted Thermo figure

    Herman Geuvers committed
Commits on Mar 24, 2010
  1. @Eelis

    ITP: Various improvements and shortenings.

    Eelis committed
    Ignore-this: 3c36131e57a7dfc9e293d76ab4fccfc4
    
    darcs-hash:20100324204311-bab43-3fc9a163dd5bbada82503f4e9ba520f079466d63.gz
  2. @Eelis

    Merge introduction and motivation sections in ITP paper. Saves one page.

    Eelis committed
    Ignore-this: 6b8537a38e3e5651475431178e8d9265
    
    darcs-hash:20100324175748-bab43-835811384164ce8ce3f4253713f8f25f24ab492c.gz
Something went wrong with that request. Please try again.