structure 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 FilterDetailsProps.instFromJsonRpcEncodablePacket : Lean.FromJson FilterDetailsProps.RpcEncodablePacket✝

Equations

• FilterDetailsProps.instFromJsonRpcEncodablePacket = { fromJson? := FilterDetailsProps.fromJsonRpcEncodablePacket✝ }

instance FilterDetailsProps.instToJsonRpcEncodablePacket : Lean.ToJson FilterDetailsProps.RpcEncodablePacket✝

Equations

• FilterDetailsProps.instToJsonRpcEncodablePacket = { toJson := FilterDetailsProps.toJsonRpcEncodablePacket✝ }

instance FilterDetailsProps.instRpcEncodable : Lean.Server.RpcEncodable FilterDetailsProps

Equations

• FilterDetailsProps.instRpcEncodable = { rpcEncode := FilterDetailsProps.instRpcEncodable.enc✝, rpcDecode := FilterDetailsProps.instRpcEncodable.dec✝ }

def FilterDetails : ProofWidgets.Component 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.