## Stream: general

### Topic: Defining decimals / trouble with dec_trivial

#### Daniel Fabian (Aug 01 2020 at 18:27):

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 (Aug 01 2020 at 18:34):

lemma is for theorems

#### Daniel Fabian (Aug 01 2020 at 18:35):

ah right, sorry, fixed

#### Daniel Fabian (Aug 01 2020 at 18:35):

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

#### Daniel Fabian (Aug 01 2020 at 18:36):

but still not with dec_trivial.

Last updated: May 08 2021 at 19:11 UTC