How to call accepts DFA

Stream: new members

[TessaCoil]

I found I could do

#eval DFA.eval {step := fun a b => b+1, start := 0, accept := ({1} : Finset Nat) : DFA Nat Nat} [0]

however if I try to call

#eval DFA.accepts {step := fun a b => b+1, start := 0, accept := ({1} : Finset Nat) : DFA Nat Nat} [0]

I get

failed to synthesize
Decidable (DFA.accepts { step := fun a b => b + 1, start := 0, accept := ↑{1} } [0])

I think I've traced the problem back to finite vs infinite sets:

def setContains: (Nat → Set Nat → Prop) :=
fun a b => a ∈ b

#eval setContains 3 ({3} : Set Nat)

says

failed to synthesize
Decidable (setContains 3 {3})

If I do

def setContainsFinset : (Nat → Finset Nat → Prop) :=
fun a b => a ∈ b

#eval setContainsFinset 3 ({3} : Finset Nat)

I still get the same error, however since it is Finset I can instead change the Prop to Bool

def setContainsFinsetBool : (Nat → Finset Nat → Bool) :=
fun a b => a ∈ b

#eval setContainsFinsetBool 3 ({3} : Finset Nat)

And it actually works with no error.

Is there a way to force this kind of behavior when calling

#eval DFA.accepts {step := fun a b => b+1, start := 0, accept := ({1} : Finset Nat) : DFA Nat Nat} [0]

?

My understanding is that this requires me to use something that is a Fintype but is there a way to do it with sets like Nat?

[Kevin Buzzard]

Thanks for your question! Can you edit your post and wrap your code with lines just containing ``` ? Then it will display a lot more nicely. For more hints on how to ask a good question see #mwe