MINDLESS C0DING

https://github.com/jonleivent/mindless-coding

Specifications, such as the dependently-typed inductive definitions of avltree and rbtree, and the dependently-typed arguments and results of their functions, are made sufficiently complete so as to constrain any implementation that type-checks to be fully correct. For example, the avltree and rbtree types both include a contents index that constrains each tree to contain exactly the specified contents in exactly the specified (sorted) order. Performance-related properties are not included - but this might be pursued in the future.

Please, stop. Being a nigger and presenting type-systems as something other than aspie toy is not an excuse to play type tetris, instead of doing actual work, like helping people and earning bucks. While you nigger-rigging your factorial correctness proof, the Ruby guy would already roll out several rails sites.