Skip to content

Instantly share code, notes, and snippets.

@fpvandoorn
Created February 3, 2020 21:23
Show Gist options
  • Save fpvandoorn/7d12927273c1168a6abc20faa403b22d to your computer and use it in GitHub Desktop.
Save fpvandoorn/7d12927273c1168a6abc20faa403b22d to your computer and use it in GitHub Desktop.
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
2020-02-03T19:39:15.8869163Z -- topology/metric_space/isometry.lean
2020-02-03T19:39:15.8869464Z #print isometric /- inhabited instance missing -/
2020-02-03T19:39:15.8869527Z
2020-02-03T19:39:15.8869824Z -- topology/metric_space/gromov_hausdorff_realized.lean
2020-02-03T19:39:15.8870472Z #print Gromov_Hausdorff.optimal_GH_coupling /- inhabited instance missing -/
2020-02-03T19:39:15.8870546Z
2020-02-03T19:39:15.8870835Z -- topology/metric_space/gromov_hausdorff.lean
2020-02-03T19:39:15.8871159Z #print Gromov_Hausdorff.GH_space.rep /- inhabited instance missing -/
2020-02-03T19:39:15.8871490Z #print Gromov_Hausdorff.aux_gluing_struct /- inhabited instance missing -/
2020-02-03T19:39:15.8871661Z
2020-02-03T19:39:15.8871964Z -- topology/local_homeomorph.lean
2020-02-03T19:39:15.8872273Z #print local_homeomorph /- inhabited instance missing -/
2020-02-03T19:39:15.8872334Z
2020-02-03T19:39:15.8872604Z -- topology/homeomorph.lean
2020-02-03T19:39:15.8872973Z #print homeomorph /- inhabited instance missing -/
2020-02-03T19:39:15.8873036Z
2020-02-03T19:39:15.8873314Z -- topology/category/UniformSpace.lean
2020-02-03T19:39:15.8873623Z #print CpltSepUniformSpace /- inhabited instance missing -/
2020-02-03T19:39:15.8873687Z
2020-02-03T19:39:15.8873979Z -- topology/category/TopCommRing.lean
2020-02-03T19:39:15.8874276Z #print TopCommRing /- inhabited instance missing -/
2020-02-03T19:39:15.8874336Z
2020-02-03T19:39:15.8874605Z -- topology/algebra/module.lean
2020-02-03T19:39:15.8874916Z #print continuous_linear_equiv /- inhabited instance missing -/
2020-02-03T19:39:15.8874978Z
2020-02-03T19:39:15.8875240Z -- set_theory/zfc.lean
2020-02-03T19:39:15.8875534Z #print pSet.type /- inhabited instance missing -/
2020-02-03T19:39:15.8875601Z
2020-02-03T19:39:15.8875869Z -- set_theory/surreal.lean
2020-02-03T19:39:15.8876168Z #print pgame.inv_ty /- inhabited instance missing -/
2020-02-03T19:39:15.8876230Z
2020-02-03T19:39:15.8876492Z -- set_theory/pgame.lean
2020-02-03T19:39:15.8876799Z #print pgame.relabelling /- inhabited instance missing -/
2020-02-03T19:39:15.8877106Z #print pgame.left_moves /- inhabited instance missing -/
2020-02-03T19:39:15.8877416Z #print pgame.right_moves /- inhabited instance missing -/
2020-02-03T19:39:15.8877723Z #print pgame.restricted /- inhabited instance missing -/
2020-02-03T19:39:15.8877799Z
2020-02-03T19:39:15.8878065Z -- set_theory/ordinal.lean
2020-02-03T19:39:15.8878348Z #print initial_seg /- inhabited instance missing -/
2020-02-03T19:39:15.8878426Z
2020-02-03T19:39:15.8878687Z -- ring_theory/maps.lean
2020-02-03T19:39:15.8878972Z #print ring_anti_equiv /- inhabited instance missing -/
2020-02-03T19:39:15.8879049Z
2020-02-03T19:39:15.8879322Z -- ring_theory/algebra.lean
2020-02-03T19:39:15.8879617Z #print alg_hom /- inhabited instance missing -/
2020-02-03T19:39:15.8879675Z
2020-02-03T19:39:15.8879937Z -- order/order_iso.lean
2020-02-03T19:39:15.8880232Z #print order_iso /- inhabited instance missing -/
2020-02-03T19:39:15.8880521Z #print order_embedding /- inhabited instance missing -/
2020-02-03T19:39:15.8880599Z
2020-02-03T19:39:15.8880870Z -- order/galois_connection.lean
2020-02-03T19:39:15.8881156Z #print galois_insertion /- inhabited instance missing -/
2020-02-03T19:39:15.8881233Z
2020-02-03T19:39:15.8881509Z -- number_theory/dioph.lean
2020-02-03T19:39:15.8881786Z #print poly /- inhabited instance missing -/
2020-02-03T19:39:15.8882095Z #print vector3 /- inhabited instance missing -/
2020-02-03T19:39:15.8882554Z #print fin2 /- inhabited instance missing -/
2020-02-03T19:39:15.8882616Z
2020-02-03T19:39:15.8882897Z -- measure_theory/measurable_space.lean
2020-02-03T19:39:15.8883205Z #print measurable_equiv /- inhabited instance missing -/
2020-02-03T19:39:15.8883290Z
2020-02-03T19:39:15.8883544Z -- linear_algebra/dual.lean
2020-02-03T19:39:15.8883838Z #print dual_pair /- inhabited instance missing -/
2020-02-03T19:39:15.8883911Z
2020-02-03T19:39:15.8884161Z -- linear_algebra/basic.lean
2020-02-03T19:39:15.8884461Z #print linear_equiv /- inhabited instance missing -/
2020-02-03T19:39:15.8884541Z
2020-02-03T19:39:15.8884801Z -- group_theory/presented_group.lean
2020-02-03T19:39:15.8885105Z #print presented_group /- inhabited instance missing -/
2020-02-03T19:39:15.8885181Z
2020-02-03T19:39:15.8885621Z -- geometry/manifold/smooth_manifold_with_corners.lean
2020-02-03T19:39:15.8885938Z #print model_with_corners /- inhabited instance missing -/
2020-02-03T19:39:15.8886016Z
2020-02-03T19:39:15.8886277Z -- geometry/manifold/real_instances.lean
2020-02-03T19:39:15.8886587Z #print euclidean_half_space /- inhabited instance missing -/
2020-02-03T19:39:15.8886895Z #print euclidean_space /- inhabited instance missing -/
2020-02-03T19:39:15.8887324Z #print euclidean_quadrant /- inhabited instance missing -/
2020-02-03T19:39:15.8887386Z
2020-02-03T19:39:15.8887661Z -- geometry/manifold/manifold.lean
2020-02-03T19:39:15.8887969Z #print structure_groupoid /- inhabited instance missing -/
2020-02-03T19:39:15.8888267Z #print pregroupoid /- inhabited instance missing -/
2020-02-03T19:39:15.8888570Z #print structomorph /- inhabited instance missing -/
2020-02-03T19:39:15.8888864Z #print manifold_core /- inhabited instance missing -/
2020-02-03T19:39:15.8888939Z
2020-02-03T19:39:15.8889221Z -- geometry/manifold/basic_smooth_bundle.lean
2020-02-03T19:39:15.8889519Z #print tangent_space /- inhabited instance missing -/
2020-02-03T19:39:15.8889838Z #print basic_smooth_bundle_core /- inhabited instance missing -/
2020-02-03T19:39:15.8890148Z #print tangent_bundle /- inhabited instance missing -/
2020-02-03T19:39:15.8890207Z
2020-02-03T19:39:15.8890468Z -- data/real/ereal.lean
2020-02-03T19:39:15.8890760Z #print ereal /- inhabited instance missing -/
2020-02-03T19:39:15.8890838Z
2020-02-03T19:39:15.8891086Z -- data/pequiv.lean
2020-02-03T19:39:15.8891383Z #print pequiv /- inhabited instance missing -/
2020-02-03T19:39:15.8891458Z
2020-02-03T19:39:15.8891698Z -- data/holor.lean
2020-02-03T19:39:15.8891994Z #print holor_index /- inhabited instance missing -/
2020-02-03T19:39:15.8892070Z
2020-02-03T19:39:15.8892315Z -- data/hash_map.lean
2020-02-03T19:39:15.8892609Z #print hash_map /- inhabited instance missing -/
2020-02-03T19:39:15.8892684Z
2020-02-03T19:39:15.8892935Z -- data/equiv/local_equiv.lean
2020-02-03T19:39:15.8893246Z #print local_equiv /- inhabited instance missing -/
2020-02-03T19:39:15.8893322Z
2020-02-03T19:39:15.8893567Z -- data/equiv/basic.lean
2020-02-03T19:39:15.8893860Z #print equiv /- inhabited instance missing -/
2020-02-03T19:39:15.8893933Z
2020-02-03T19:39:15.8894179Z -- data/equiv/algebra.lean
2020-02-03T19:39:15.8894475Z #print add_equiv /- inhabited instance missing -/
2020-02-03T19:39:15.8894774Z #print mul_equiv /- inhabited instance missing -/
2020-02-03T19:39:15.8894837Z
2020-02-03T19:39:15.8895111Z -- data/analysis/topology.lean
2020-02-03T19:39:15.8895414Z #print ctop.realizer /- inhabited instance missing -/
2020-02-03T19:39:15.8895707Z #print ctop /- inhabited instance missing -/
2020-02-03T19:39:15.8895764Z
2020-02-03T19:39:15.8896030Z -- data/analysis/filter.lean
2020-02-03T19:39:15.8896339Z #print filter.realizer /- inhabited instance missing -/
2020-02-03T19:39:15.8896638Z #print cfilter /- inhabited instance missing -/
2020-02-03T19:39:15.8896695Z
2020-02-03T19:39:15.8896960Z -- data/W.lean
2020-02-03T19:39:15.8897242Z #print W /- inhabited instance missing -/
2020-02-03T19:39:15.8897298Z
2020-02-03T19:39:15.8897583Z -- category_theory/natural_transformation.lean
2020-02-03T19:39:15.8897894Z #print category_theory.nat_trans /- inhabited instance missing -/
2020-02-03T19:39:15.8897958Z
2020-02-03T19:39:15.8898238Z -- category_theory/monoidal/functor.lean
2020-02-03T19:39:15.8898562Z #print category_theory.lax_monoidal_functor /- inhabited instance missing -/
2020-02-03T19:39:15.8898903Z #print category_theory.monoidal_functor /- inhabited instance missing -/
2020-02-03T19:39:15.8898970Z
2020-02-03T19:39:15.8899245Z -- category_theory/monad/algebra.lean
2020-02-03T19:39:15.8899561Z #print category_theory.monad.algebra /- inhabited instance missing -/
2020-02-03T19:39:15.8899626Z
2020-02-03T19:39:15.8899913Z -- category_theory/limits/shapes/pullbacks.lean
2020-02-03T19:39:15.8900237Z #print category_theory.limits.walking_span /- inhabited instance missing -/
2020-02-03T19:39:15.8900694Z #print category_theory.limits.walking_cospan.hom /- inhabited instance missing -/
2020-02-03T19:39:15.8901017Z #print category_theory.limits.walking_cospan /- inhabited instance missing -/
2020-02-03T19:39:15.8901356Z #print category_theory.limits.walking_span.hom /- inhabited instance missing -/
2020-02-03T19:39:15.8901441Z
2020-02-03T19:39:15.8901710Z -- category_theory/limits/shapes/equalizers.lean
2020-02-03T19:39:15.8902056Z #print category_theory.limits.walking_parallel_pair_hom /- inhabited instance missing -/
2020-02-03T19:39:15.8902514Z #print category_theory.limits.walking_parallel_pair /- inhabited instance missing -/
2020-02-03T19:39:15.8902604Z
2020-02-03T19:39:15.8902880Z -- category_theory/limits/shapes/binary_products.lean
2020-02-03T19:39:15.8903206Z #print category_theory.limits.walking_pair /- inhabited instance missing -/
2020-02-03T19:39:15.8903288Z
2020-02-03T19:39:15.8903545Z -- category_theory/limits/limits.lean
2020-02-03T19:39:15.8903876Z #print category_theory.limits.is_limit /- inhabited instance missing -/
2020-02-03T19:39:15.8904220Z #print category_theory.limits.is_colimit /- inhabited instance missing -/
2020-02-03T19:39:15.8904286Z
2020-02-03T19:39:15.8904556Z -- category_theory/limits/cones.lean
2020-02-03T19:39:15.8904871Z #print category_theory.limits.cone /- inhabited instance missing -/
2020-02-03T19:39:15.8905195Z #print category_theory.limits.cocone /- inhabited instance missing -/
2020-02-03T19:39:15.8905263Z
2020-02-03T19:39:15.8905532Z -- category_theory/functor.lean
2020-02-03T19:39:15.8905843Z #print category_theory.functor /- inhabited instance missing -/
2020-02-03T19:39:15.8905908Z
2020-02-03T19:39:15.8906180Z -- category_theory/equivalence.lean
2020-02-03T19:39:15.8906493Z #print category_theory.equivalence /- inhabited instance missing -/
2020-02-03T19:39:15.8906554Z
2020-02-03T19:39:15.8906823Z -- category_theory/endomorphism.lean
2020-02-03T19:39:15.8907130Z #print category_theory.End /- inhabited instance missing -/
2020-02-03T19:39:15.8907199Z
2020-02-03T19:39:15.8907476Z -- category_theory/elements.lean
2020-02-03T19:39:15.8907795Z #print category_theory.functor.elements /- inhabited instance missing -/
2020-02-03T19:39:15.8907859Z
2020-02-03T19:39:15.8908143Z -- category_theory/concrete_category/bundled.lean
2020-02-03T19:39:15.8908458Z #print category_theory.bundled /- inhabited instance missing -/
2020-02-03T19:39:15.8908521Z
2020-02-03T19:39:15.8908793Z -- category_theory/category/Cat.lean
2020-02-03T19:39:15.8909109Z #print category_theory.Cat /- inhabited instance missing -/
2020-02-03T19:39:15.8909170Z
2020-02-03T19:39:15.8909448Z -- category_theory/adjunction/basic.lean
2020-02-03T19:39:15.8909764Z #print category_theory.adjunction /- inhabited instance missing -/
2020-02-03T19:39:15.8909827Z
2020-02-03T19:39:15.8910091Z -- category/functor.lean
2020-02-03T19:39:15.8910391Z #print functor.comp /- inhabited instance missing -/
2020-02-03T19:39:15.8910451Z
2020-02-03T19:39:15.8910733Z -- algebraic_geometry/presheafed_space.lean
2020-02-03T19:39:15.8911068Z #print algebraic_geometry.PresheafedSpace /- inhabited instance missing -/
2020-02-03T19:39:15.8911407Z #print algebraic_geometry.PresheafedSpace.hom /- inhabited instance missing -/
2020-02-03T19:39:15.8911474Z
2020-02-03T19:39:15.8911733Z -- algebra/ring.lean
2020-02-03T19:39:15.8912025Z #print ring_hom /- inhabited instance missing -/
2020-02-03T19:39:15.8912083Z
2020-02-03T19:39:15.8912348Z -- algebra/lie_algebra.lean
2020-02-03T19:39:15.8912658Z #print lie_submodule /- inhabited instance missing -/
2020-02-03T19:39:15.8912963Z #print lie_subalgebra /- inhabited instance missing -/
2020-02-03T19:39:15.8913278Z #print lie_algebra.morphism /- inhabited instance missing -/
2020-02-03T19:39:15.8913339Z
2020-02-03T19:39:15.8913603Z -- algebra/direct_limit.lean
2020-02-03T19:39:15.8913923Z #print add_comm_group.direct_limit /- inhabited instance missing -/
2020-02-03T19:39:15.8913986Z
2020-02-03T19:39:15.8914259Z -- algebra/category/Module/basic.lean
2020-02-03T19:39:15.8914554Z #print Module /- inhabited instance missing -/
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment