How to construct a frame with two elements

Stream: new members

[Christian Corbett]

Hello,
I am trying to construct a frame {0,1} consisting of only two elements. In lieu of building it manually, I am using the fact that Lean recognizes Prop as an object in the typeclass Frame:

import Mathlib.Order.CompleteBooleanAlgebra
open Order
#check (inferInstance : Frame Prop)

However, I am wary that there might be some conflicts that arise when using Prop as a two element frame. I tried using Bool:

#check (inferInstance : Frame Bool)

but this fails in Lean. Does anyone have any recommendations about how they would construct a two element frame?

[Christian Corbett]

Oops, I realized I needed

import Mathlib.Data.Fintype.Order

for

#check (inferInstance : Frame Bool)

to pass. I'm still unsure if this is the best way to construct a two element frame in Lean.

[Eric Wieser]

Generally I would recommend import Mathlib when trying to answer the question "does this instance exist"

[Matt Diamond]

also, you can do #synth Frame Bool