CSLib grind sets

This module registers custom grind sets in CSLib.

def Cslib.Logic.Modal.Lean.Parser.Attr.modal : Lean.ParserDescr

The modal grind set is designed to quickly resolve goals that can be derived from modal reasoning without unfolding the underlying Lean semantics of satisfaction for modalities. Use this in combination with modal axioms for more powerful proof search.

Equations

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

def Cslib.Logic.Modal.Lean.Parser.Attr.modal! : Lean.ParserDescr

The modal grind set is designed to quickly resolve goals that can be derived from modal reasoning without unfolding the underlying Lean semantics of satisfaction for modalities. Use this in combination with modal axioms for more powerful proof search.

Equations

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

def Cslib.Logic.Modal.Lean.Parser.Attr.modal!? : Lean.ParserDescr

The modal grind set is designed to quickly resolve goals that can be derived from modal reasoning without unfolding the underlying Lean semantics of satisfaction for modalities. Use this in combination with modal axioms for more powerful proof search.

Equations

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

def Cslib.Logic.Modal.Lean.Parser.Attr.modal? : Lean.ParserDescr

The modal grind set is designed to quickly resolve goals that can be derived from modal reasoning without unfolding the underlying Lean semantics of satisfaction for modalities. Use this in combination with modal axioms for more powerful proof search.

Equations

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