Skip to content

History

Revisions

  • Write Tradeoffs of concrete types defined as subobjects

    @YaelDillies YaelDillies committed Jul 25, 2024
    6e895c4

  • Destroyed port comments (markdown)

    @jcommelin jcommelin committed Jul 18, 2024
    aaed9b5

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    014de59

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    d77de61

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    cd791db

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    5ad3aaf

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    6fc1307

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    ed7f880

  • Created Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    de96413

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed May 17, 2024
    5e42b08

  • Updated Computation models for polynomials and finitely supported functions (markdown)

    @eric-wieser eric-wieser committed Apr 28, 2024
    a71455c

  • Updated Using mathlib4 as a dependency (markdown)

    @fpvandoorn fpvandoorn committed Apr 25, 2024
    c4265ac

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Apr 16, 2024
    d8d7b21

  • include `trace[debug]`

    @thorimur thorimur committed Mar 14, 2024
    8070de7

  • note on `run`/`lift``TermElabM`

    @thorimur thorimur committed Mar 8, 2024
    9023dcb

  • Revert 00a26fcf11aac8b845f09e21bd1066a3d89fdb6a...406b6e8101a7c0e8ab9bffc122d12a7965845220 on Monad map

    @thorimur thorimur committed Mar 6, 2024
    b7fb8cb

  • use `?pattern=` instead of full module name in url

    @thorimur thorimur committed Mar 6, 2024
    406b6e8

  • edge label links

    @thorimur thorimur committed Mar 6, 2024
    00a26fc

  • update Simp.M info

    @thorimur thorimur committed Mar 6, 2024
    c7549a7

  • remove unsupported target='_blank'

    @thorimur thorimur committed Mar 6, 2024
    1487761

  • restore links to nodes; point to docs page instead of query

    @thorimur thorimur committed Mar 6, 2024
    79f4cf6

  • Updated Monad map (markdown)

    @thorimur thorimur committed Feb 29, 2024
    961b8c8

  • Added zulip thread according to https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Why.20is.20.60Polynomial.60.20noncomputable.3F/near/422268732

    @qawbecrdtey qawbecrdtey committed Feb 19, 2024
    71f1e3c

  • html formatting broke; partial workaround using click functionality

    @thorimur thorimur committed Feb 8, 2024
    9934995

  • link not a bullet

    @madvorak madvorak committed Jan 29, 2024
    614dc7d

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Jan 16, 2024
    8a1361d

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Jan 16, 2024
    5a3ed5c

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Jan 16, 2024
    d5706f3

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Jan 16, 2024
    40dc7a3

  • Created Metaprogramming gotchas (markdown)

    @kmill kmill committed Jan 11, 2024
    51912d3