Revision ad46491be091e941cc7489d8ef77110abdcfffb8 authored by Johan Commelin on 27 June 2020, 09:48:47 UTC, committed by Johan Commelin on 27 June 2020, 09:48:47 UTC
1 parent 23c2b19
File | Mode | Size |
---|---|---|
conv | ||
library_search | ||
localized | ||
monotonicity | ||
transport | ||
abel.lean | -rw-r--r-- | 250 bytes |
apply.lean | -rw-r--r-- | 1.0 KB |
apply_fun.lean | -rw-r--r-- | 827 bytes |
back_chaining.lean | -rw-r--r-- | 751 bytes |
cancel_denoms.lean | -rw-r--r-- | 398 bytes |
choose.lean | -rw-r--r-- | 852 bytes |
coinductive.lean | -rw-r--r-- | 5.2 KB |
conv.lean | -rw-r--r-- | 1.2 KB |
convert.lean | -rw-r--r-- | 594 bytes |
delta_instance.lean | -rw-r--r-- | 836 bytes |
differentiable.lean | -rw-r--r-- | 1.9 KB |
doc_commands.lean | -rw-r--r-- | 159 bytes |
equiv_rw.lean | -rw-r--r-- | 8.9 KB |
examples.lean | -rw-r--r-- | 2.1 KB |
expr.lean | -rw-r--r-- | 342 bytes |
expr_lens.lean | -rw-r--r-- | 1.2 KB |
ext.lean | -rw-r--r-- | 2.9 KB |
fin_cases.lean | -rw-r--r-- | 2.1 KB |
finish1.lean | -rw-r--r-- | 4.8 KB |
finish2.lean | -rw-r--r-- | 12.4 KB |
finish3.lean | -rw-r--r-- | 2.9 KB |
finish4.lean | -rw-r--r-- | 1.5 KB |
generalizes.lean | -rw-r--r-- | 3.5 KB |
group.lean | -rw-r--r-- | 1.9 KB |
hint.lean | -rw-r--r-- | 1.3 KB |
inhabit.lean | -rw-r--r-- | 392 bytes |
instance_cache.lean | -rw-r--r-- | 1.3 KB |
interval_cases.lean | -rw-r--r-- | 3.8 KB |
linarith.lean | -rw-r--r-- | 8.4 KB |
lint.lean | -rw-r--r-- | 4.2 KB |
lint_coe_t.lean | -rw-r--r-- | 1.1 KB |
lint_coe_to_fun.lean | -rw-r--r-- | 783 bytes |
lint_simp_comm.lean | -rw-r--r-- | 1.0 KB |
lint_simp_nf.lean | -rw-r--r-- | 921 bytes |
lint_simp_var_head.lean | -rw-r--r-- | 589 bytes |
local_cache.lean | -rw-r--r-- | 9.8 KB |
logic_inline.lean | -rw-r--r-- | 418 bytes |
matrix.lean | -rw-r--r-- | 649 bytes |
mk_iff_of_inductive.lean | -rw-r--r-- | 737 bytes |
mllist.lean | -rw-r--r-- | 1.5 KB |
monotonicity.lean | -rw-r--r-- | 8.0 KB |
noncomm_ring.lean | -rw-r--r-- | 2.4 KB |
norm_cast.lean | -rw-r--r-- | 4.1 KB |
norm_cast_cardinal.lean | -rw-r--r-- | 1002 bytes |
norm_cast_coe_fn.lean | -rw-r--r-- | 767 bytes |
norm_cast_int.lean | -rw-r--r-- | 568 bytes |
norm_cast_lemma_order.lean | -rw-r--r-- | 654 bytes |
norm_cast_sum_lambda.lean | -rw-r--r-- | 475 bytes |
norm_num.lean | -rw-r--r-- | 11.7 KB |
nth_rewrite.lean | -rw-r--r-- | 3.1 KB |
omega.lean | -rw-r--r-- | 3.1 KB |
packaged_goal.lean | -rw-r--r-- | 819 bytes |
pi_simp.lean | -rw-r--r-- | 652 bytes |
protec_proj.lean | -rw-r--r-- | 501 bytes |
push_neg.lean | -rw-r--r-- | 2.0 KB |
rat.lean | -rw-r--r-- | 308 bytes |
rcases.lean | -rw-r--r-- | 2.2 KB |
refine_struct.lean | -rw-r--r-- | 3.8 KB |
rename_var.lean | -rw-r--r-- | 685 bytes |
replacer.lean | -rw-r--r-- | 939 bytes |
restate_axiom.lean | -rw-r--r-- | 325 bytes |
rewrite.lean | -rw-r--r-- | 1.4 KB |
ring.lean | -rw-r--r-- | 2.0 KB |
ring_exp.lean | -rw-r--r-- | 6.2 KB |
set.lean | -rw-r--r-- | 1.0 KB |
simp_command.lean | -rw-r--r-- | 2.0 KB |
simp_result.lean | -rw-r--r-- | 3.8 KB |
simp_rw.lean | -rw-r--r-- | 1.6 KB |
simps.lean | -rw-r--r-- | 7.2 KB |
solve_by_elim.lean | -rw-r--r-- | 4.1 KB |
split_ifs.lean | -rw-r--r-- | 602 bytes |
squeeze.lean | -rw-r--r-- | 295 bytes |
suggest.lean | -rw-r--r-- | 2.6 KB |
tactics.lean | -rw-r--r-- | 15.6 KB |
tauto.lean | -rw-r--r-- | 2.4 KB |
terminal_goal.lean | -rw-r--r-- | 1.5 KB |
tidy.lean | -rw-r--r-- | 1.1 KB |
traversable.lean | -rw-r--r-- | 1.9 KB |
trunc_cases.lean | -rw-r--r-- | 2.3 KB |
where.lean | -rw-r--r-- | 8.2 KB |
with_local_reducibility.lean | -rw-r--r-- | 1.8 KB |
wlog.lean | -rw-r--r-- | 3.0 KB |
zify.lean | -rw-r--r-- | 697 bytes |
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...