Zulip Chat Archive

Stream: general

Topic: Defining decimals / trouble with dec_trivial


view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 01 2020 at 18:34):

lemma is for theorems

view this post on Zulip Daniel Fabian (Aug 01 2020 at 18:35):

ah right, sorry, fixed

view this post on Zulip Daniel Fabian (Aug 01 2020 at 18:35):

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

view this post on Zulip Daniel Fabian (Aug 01 2020 at 18:36):

but still not with dec_trivial.


Last updated: May 08 2021 at 19:11 UTC