Gabriel Ebner 2e142d87ae fix(library/init/data/repr): give correct implementation of nat.repr		2017-06-19 16:20:27 +02:00
..
algebra	feat(init/data/int,init/data/nat,init/algebra): more algebra theorems	2017-06-01 15:15:40 -07:00
category	feat(library/init/meta): corec_on for coinductive predicates	2017-06-12 20:42:48 -07:00
data	fix(library/init/data/repr): give correct implementation of nat.repr	2017-06-19 16:20:27 +02:00
meta	fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean	2017-06-18 18:33:27 -07:00
native	fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean	2017-06-18 18:33:27 -07:00
cc_lemmas.lean
classical.lean	fix(library/noncomputable): fixes #1631	2017-05-31 23:16:37 -07:00
coe.lean	chore(library): convert comments to docstrings	2017-06-12 15:17:00 +02:00
core.lean	chore(library): convert comments to docstrings	2017-06-12 15:17:00 +02:00
default.lean
function.lean
funext.lean
init.md
logic.lean	chore(library): convert comments to docstrings	2017-06-12 15:17:00 +02:00
propext.lean
relator.lean	feat(init/relator): some new base theorems for transfer tactic	2017-05-27 04:16:25 -04:00
util.lean	refactor(library): has_to_string ==> has_repr	2017-06-18 18:29:19 -07:00
wf.lean