expr.pis

Stream: general

[Jakob von Raumer]

Why doesn't #reduce expr.pis [expr.local_const ` A `A binder_info.default `(Sort 1)] `(Sort 1)terminate?

[Kevin Buzzard]

In an ideal world you would go to the set_option docs and look at the section "how do I track down an excessive memory consumption error?"

[Gabriel Ebner]

@Jakob von Raumer You should use #eval since expr.pis is meta.

[Gabriel Ebner]

And I think the following should explain why kernel reduction fails on this example:

set_option pp.all true
#print raw `A
/-
name.mk_string
  (string.str string.empty
     (char.of_nat
        (@bit1.{0} nat nat.has_one nat.has_add
           (@bit0.{0} nat nat.has_add
              (@bit0.{0} nat nat.has_add
                 (@bit0.{0} nat nat.has_add
                    (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)))))))))
  name.anonymous
-/

[Gabriel Ebner]

(I just tried all subterms of the example, and already #reduce `A fails.)

[Jakob von Raumer]

Thanks :)

[Jakob von Raumer]

But for #eval I'm getting a "result type does not have an instance of type class 'has_repr', dumping internal representation"?

[Gabriel Ebner]

meta instance: has_repr expr := ⟨expr.to_string⟩

:smile: I'm not sure if Leo would like a PR though...