decidable_pred

Stream: new members

[Julian Berman]

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?

[Julian Berman]

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

[Julian Berman]

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}.

[Scott Morrison]

open_locale classical