# Zulip Chat Archive

## Stream: general

### Topic: help with `has_to_pexpr`

#### Scott Morrison (May 23 2020 at 13:46):

I'm not sure how to construct `has_to_pexpr`

instances, and there are few useful examples around. In particular, I'd like to make the following work:

```
import tactic
open tactic
meta instance nat_pexpr : has_to_pexpr ℕ := ⟨pexpr.of_expr ∘ λ n, reflect n⟩
meta instance int_pexpr : has_to_pexpr ℤ := ⟨pexpr.of_expr ∘ λ n, reflect n⟩
meta def turkle (p : ℕ) : tactic unit :=
do M ← to_expr ``(2^%%p - 1 : ℤ) >>= eval_expr ℤ,
t ← to_expr ``(2^%%p - 1 = %%M),
v ← to_expr ``(by norm_num : 2^%%p - 1 = %%M),
assertv `w t v,
skip
example : true :=
begin
turkle 5,
-- This produces `w : 2^5 - 1 = int.of_nat 31`,
-- but I want:
guard_hyp w := 2^5 - 1 = (31 : ℤ),
trivial,
end
```

#### Scott Morrison (May 23 2020 at 13:48):

I guess this is the `int_pexpr`

instance's fault, but I don't know what to replace it with.

#### Scott Morrison (May 23 2020 at 13:55):

Oh... maybe I undestand. I just have to calculate the binary digits of my integer, and build the `pexpr`

out of `bit0`

and `bit1`

directly? (And put in a negative sign if the integer is negative...)

#### Scott Morrison (May 23 2020 at 13:56):

Does this exist somewhere already? It seems like the sort of thing that someone would have wanted before me.

#### Scott Morrison (May 23 2020 at 14:15):

Alternatively, adding ``[simp at w]`

at the end of `turkle`

achieves the desired result, so I'm going to leave this for now.

#### Reid Barton (May 23 2020 at 14:17):

Presumably whatever is building `int.of_nat 31`

already knows how to do the `bit0`

/`bit1`

part.

#### Simon Hudon (May 23 2020 at 17:20):

You may want to look at the `has_reflect`

instance for `nat`

. I believe that's where the `bit0 / bit1`

logic is. My guess is that `has_reflect`

on `int`

is done by pattern matching on the `int`

, reflecting the `nat`

and then applying the constructor. Instead, you can treat the `int`

as a number in its own right and do the binary division and add a minus when necessary

#### Mario Carneiro (May 23 2020 at 19:42):

the `eval_expr`

on the first line is completely unnecessary, just do `let M := 2^p-1`

Last updated: May 14 2021 at 07:19 UTC