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 |
Computing file changes ...
