structure ProofWidgets.FilterDetailsProps : Type

Props for the FilterDetails component.

• summary : ProofWidgets.Html

  Contents of the <summary>.

• filtered : ProofWidgets.Html

  What is shown in the filtered state.

• all : ProofWidgets.Html

  What is shown in the non-filtered state.

• initiallyFiltered : Bool

  Whether to start in the filtered state.

instance ProofWidgets.instRpcEncodableFilterDetailsProps : Lean.Server.RpcEncodable ProofWidgets.FilterDetailsProps

Equations

• ProofWidgets.instRpcEncodableFilterDetailsProps = { rpcEncode := ProofWidgets.instRpcEncodableFilterDetailsProps.enc✝, rpcDecode := ProofWidgets.instRpcEncodableFilterDetailsProps.dec✝ }

def ProofWidgets.FilterDetails : ProofWidgets.Component ProofWidgets.FilterDetailsProps

The FilterDetails component is like a <details> HTML element, but also has a filter button that allows you to switch between filtered and unfiltered states.

Equations

• One or more equations did not get rendered due to their size.