Zulip Chat Archive

Stream: general

Topic: dsimp_config


view this post on Zulip Edward Ayers (Oct 10 2018 at 12:26):

Please could someone help me fill in these holes in the docstring for dsimp_config?

structure dsimp_config :=
(md                        := reducible) -- reduction mode: how aggressively constants are replaced with their definitions.
(max_steps : nat           := simp.default_max_steps) -- The maximum number of steps allowed before failing.
(canonize_instances : bool := tt) -- [TODO] ???
(single_pass : bool        := ff) -- [TODO] Does this mean that _each_ simp-lemma can only be used once?
(fail_if_unchanged         := tt) -- Don't throw if simp didn't do anything.
(eta                       := tt) -- allow eta-equivalence: `(λ x, F $ x) ↝ F`
(zeta : bool               := tt) -- do zeta-reductions: `let x : a := b in c ↝ c[x/b]`.
(beta : bool               := tt) -- do beta-reductions: `(λ x, E) $ (y) ↝ E[x/y]`.
(proj : bool               := tt) -- reduce projections: `⟨a,b⟩.1 ↝ a` [TODO] I think?
(iota : bool               := tt) -- reduce recursors for inductive datatypes: eg `nat.rec_on (succ n) Z R ↝ R n $ nat.rec_on n Z R`
(unfold_reducible          := ff) -- if tt, definitions with `reducible` transparency will be unfolded (delta-reduced)
(memoize                   := tt) -- [TODO] what is being memoised?

view this post on Zulip Edward Ayers (Oct 10 2018 at 12:29):

(I'm working through init/meta in the Lean source and adding all the missing docstrings)

view this post on Zulip Chris Hughes (Nov 15 2018 at 20:54):

@Edward Ayers Is a copy of your Lean with docstring available online anywhere? It would be really useful.

view this post on Zulip Edward Ayers (Nov 16 2018 at 10:57):

https://github.com/EdAyers/lean

view this post on Zulip Edward Ayers (Nov 16 2018 at 10:58):

Checkout the doc branch

view this post on Zulip Edward Ayers (Nov 16 2018 at 10:59):

I use the build from that branch as my main lean executable

view this post on Zulip Patrick Massot (Nov 16 2018 at 11:00):

Do you mean you added stuff besides docstrings?

view this post on Zulip Edward Ayers (Nov 16 2018 at 11:00):

No I haven't added anything except docstrings on that branch

view this post on Zulip Edward Ayers (Nov 16 2018 at 11:01):

(hopefully, no guarantees)

view this post on Zulip Edward Ayers (Nov 16 2018 at 11:01):

It builds mathlib though so its probably fine. I didn't sneak in false as an axiom anywhere.

view this post on Zulip Edward Ayers (Nov 16 2018 at 11:02):

I also can't guarantee that the docstrings I added aren't misleading, they are more a side-effect of me trying to understand the sourcecode

view this post on Zulip Chris Hughes (Nov 16 2018 at 11:07):

Thanks @Edward Ayers


Last updated: May 08 2021 at 09:11 UTC