Defining decimals / trouble with dec_trivial

Stream: general

[Daniel Fabian]

I'm trying to define decimals, so that I can define to_string for smtlib. So far, I've got a definition that should in principle work, I think. It is a decidable proposition and when run as a tactic, it works fine, but for whatever reason, the kernel refuses to evaluate it:

import tactic

@[derive decidable_eq]
structure decimal := (d : ℚ) (is_decimal : d.denom.factors.to_finset ⊆ {2, 5})

lemma fails := decimal.mk (2.5) dec_trivial

lemma succeed : (2.5 : ℚ).denom.factors.head ∈ [2, 5] := dec_trivial

def succeed2 (q : ℚ) : option decimal :=
if h : q.denom.factors.to_finset ⊆ {2, 5} then some $ decimal.mk q h else none

meta def check_num (q : ℚ) : tactic unit :=
do  dec ← succeed2 q,
    tactic.trace dec.d,
    return ()

run_cmd check_num 2.5
#eval (succeed2 2.5).map (λ x, decimal.d x)

Any idea what I'm doing wrong? What I'm trying to do, is define a type decimal, such that I can write dec 2.6, dec 3/4 but not dec 1/3. As the latter cannot be turned into a string.

[Reid Barton]

lemma is for theorems

[Daniel Fabian]

ah right, sorry, fixed

[Daniel Fabian]

ok, cool, now it can be used in the tactic.

[Daniel Fabian]

but still not with dec_trivial.