lean4-htt/library
Leonardo de Moura 6887a99f08 feat(library/init/category/state): make state and state_t universe polymorphic
The new definitions are not fully general since they force data and
state to be in the same universe.
2017-03-22 23:45:29 -07:00
..
data feat(library/system/io): system.io without axioms 2017-03-22 23:36:05 -07:00
init feat(library/init/category/state): make state and state_t universe polymorphic 2017-03-22 23:45:29 -07:00
smt fix(library/smt/prove.lean): collect_props was collecting (H : Prop) 2017-03-12 09:54:01 -07:00
system feat(library/system/io): system.io without axioms 2017-03-22 23:36:05 -07:00
tools feat(library/tactic/vm_monitor): use attribute for registering VM monitors 2017-03-22 07:34:27 -07:00
.project feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
library.md doc(fixing_broken_links) 2017-03-22 08:13:36 -07:00
standard.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00