Zulip Chat Archive

Stream: new members

Topic: decidable_pred


view this post on Zulip Julian Berman (Mar 17 2021 at 03:13):

I have this:

import data.nat.fib
import combinatorics.composition

noncomputable theory
open nat

def fibs (n : ) : finset (composition n) :=
finset.univ.filter (λ c,  i  c.blocks, i  set.range fib)

and lean is still telling me failed to synthesize type class instance for n : ℕ ⊢ decidable_pred (λ (c : composition n), ∀ (i : ℕ), i ∈ c.blocks → i ∈ set.range fib).

noncomputable theory means something like "I don't care about decidability" already right? Is the reason for the complaint there that basically Lean can't prove that set is a finset?

view this post on Zulip Julian Berman (Mar 17 2021 at 03:26):

OK I guess I see, finset.filter says what you give it has to be decidable regardless of what I did in my file

view this post on Zulip Julian Berman (Mar 17 2021 at 03:28):

I guess using a set works then instead since I don't really care whether it's finite or not def fibs (n : ℕ) : set (composition n) := {c | ∀ i ∈ c.blocks, i ∈ set.range fib}.

view this post on Zulip Scott Morrison (Mar 17 2021 at 03:42):

open_locale classical


Last updated: May 08 2021 at 09:11 UTC