expr.is_internal_cnstr

Stream: general

[Edward Ayers]

What does expr.is_internal_cnstr do?

[Edward Ayers]

I've fiddled around with it but I can't get it to return anything except none.

[Edward Ayers]

In the C++ it looks like it's just checking if the expr is a constant and checking that the name of the constant ends with _cnstr. What would be an example of that?

[Edward Ayers]

Also get_nat_value, extracts a nat from a "nat value macro". But I can't see where nat value macros are used.

[Edward Ayers]

What do I need to do to get rid of the failed to synthesize type class instance for ⊢ reflected e error?

universes u v
def e := Π a : Type u, Π b : Type v, a × b
#check e
#eval to_string $ expr.collect_univ_params $ `(e)

[Simon Hudon]

I think is_internal_cnstr will rarely give you an answer. When it does, your expression will likely give you a bunch of trouble and that's why I wrote tactic.pis in mathlib to replace expr.pis.

[Simon Hudon]

What do I need to do to get rid of the failed to synthesize type class instance for ⊢ reflected e error?

universes u v
def e := Π a : Type u, Π b : Type v, a × b
#check e
#eval to_string $ expr.collect_univ_params $ `(e)

I don't know if there is a reflected instance for types in general. You may have to go through to_expr