fpvandoorn

import Mathlib

open Lean Meta Elab Command

-- generalized
/-- Write an import graph, represented as a an array of `NameMap`s to the ".dot" graph format.
  If `("style1", graph1)` is in `graphs`, then the edges in `graph1` will be labeled with `[style1]`.
  Example: `asStyledDotGraph #[("", graph1), ("style=dashed", graph2)]` -/
def asStyledDotGraph [ForIn Id α Name] (graphs : Array (String × NameMap α))
    (header := "import_graph") : String := Id.run do

fpvandoorn

import Mathlib.Tactic.LibrarySearch
import Mathlib.Tactic.Propose

open Lean Elab Server Lsp RequestM Parser Mathlib Tactic LibrarySearch Meta Std.Tactic.TryThis
  Propose

structure TryThisInfo where
  replacement : Syntax
  deriving TypeName

fpvandoorn

def read (s : String) : List (Option (Nat ⊕ Nat)) :=
s.data.map fun
| '(' => .some <| .inl 0
| '{' => .some <| .inl 1
| '[' => .some <| .inl 2
| '<' => .some <| .inl 3
| ')' => .some <| .inr 0
| '}' => .some <| .inr 1
| ']' => .some <| .inr 2
| '>' => .some <| .inr 3

fpvandoorn

import Mathlib.Init.Data.Nat.Notation
import Mathlib.Lean.Message
import Mathlib.Lean.Expr.Basic
import Mathlib.Data.String.Defs
import Mathlib.Tactic.Simps.NotationClass

open Lean Elab Parser Command
open Meta hiding Config
open Elab.Term hiding mkConst

fpvandoorn

/-
Copyright (c) 2022 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/

import Mathlib.Init.Data.Nat.Notation
import Mathlib.Lean.Message
import Mathlib.Lean.Expr.Basic
import Mathlib.Data.String.Defs

fpvandoorn

 antitone.const_mul' ← antitone.const_add,
 finset.prod_powerset_insert ← finset.sum_powerset_insert,
 dist_eq_norm_div' ← dist_eq_norm_sub',
 units.is_unit_mul_units ← add_units.is_add_unit_add_add_units,
 Group.filtered_colimits.colimit_has_inv ← AddGroup.filtered_colimits.colimit_has_neg,
 unique_mul.exists_iff_exists_exists_unique ← unique_add.exists_iff_exists_exists_unique,
 subsemigroup.mem_map ← add_subsemigroup.mem_map,
 free_group.norm ← free_add_group.norm,
 finset.prod_ite_index ← finset.sum_ite_index,
 monoid_hom.to_localization_map ← add_monoid_hom.to_localization_map,

fpvandoorn

/- Checking 74465 declarations (plus 74875 automatically generated ones) in mathlib (only in imported files) -/

/- The `check_type` linter reports: -/
/- THE STATEMENTS OF THE FOLLOWING DECLARATIONS DO NOT TYPE-CHECK.
Some definitions in the statement are marked @[irreducible], which means that the statement is now ill-formed. It is likely that these definitions were locally marked @[reducible], and that type-class instances were applied that don't apply when the definitions are @[irreducible].: -/
-- algebra\category\Mon\adjunctions.lean
#print adjoin_one.equations._eqn_1 /- The statement doesn't type-check -/
#print adjoin_zero_map /- The statement doesn't type-check -/
#print adjoin_zero.equations._eqn_1 /- The statement doesn't type-check -/
#print adjoin_one_map /- The statement doesn't type-check -/

fpvandoorn

import tactic -- all

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

fpvandoorn

2020-02-03T19:39:15.8860466Z /- TYPES ARE MISSING INHABITED INSTANCES: -/
2020-02-03T19:39:15.8860718Z 
2020-02-03T19:39:15.8861155Z -- topology/topological_fiber_bundle.lean
2020-02-03T19:39:15.8861629Z #print bundle_trivialization /- inhabited instance missing -/
2020-02-03T19:39:15.8867768Z #print topological_fiber_bundle_core /- inhabited instance missing -/
2020-02-03T19:39:15.8867878Z 
2020-02-03T19:39:15.8868166Z -- topology/opens.lean
2020-02-03T19:39:15.8868492Z #print topological_space.nonempty_compacts /- inhabited instance missing -/
2020-02-03T19:39:15.8868820Z #print topological_space.closeds /- inhabited instance missing -/
2020-02-03T19:39:15.8868884Z 

fpvandoorn

/- All declarations in mathlib that
  * are a lemma/theorem but construct data
  * are a definition, but define an element of a proposition
  
  All automatically generated definitions and all instances are filtered out.
-/

-- topology\uniform_space\uniform_embedding.lean
#print uniform_inducing.mk' -- is a def, should be a lemma/theorem