Commit graph

7 commits

Author SHA1 Message Date
Leonardo de Moura
105c29b51e refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 19:59:38 -07:00
Leonardo de Moura
c37b5afe93 feat(library/standard): add decidable class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 00:19:32 +01:00
Leonardo de Moura
c16951aba6 fix(library/aliases): aliasing behavior
The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 15:40:55 -07:00
Leonardo de Moura
d30f387e72 feat(library/standard): add namespace 'pair'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 14:48:19 -07:00
Leonardo de Moura
00e1a7db23 feat(frontends/lean/elaborator): add class instance elaboration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 15:45:50 -07:00
Leonardo de Moura
079672f6f9 feat(frontends/lean): add 'class' and 'instances' infrastructure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 14:28:09 -07:00
Leonardo de Moura
855ffcba34 feat(library/standard): add pairs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 20:43:16 -07:00