Documentation

Lean.Meta.Tactic.Grind.Types

We use this auxiliary constant to mark delayed congruence proofs.

Equations
Instances For

    Returns true if e is True, False, or a literal value. See Lean.Meta.LitValues for supported literals.

    Equations
    Instances For

      Context for GrindM monad.

      Instances For

        Key for the congruence theorem cache.

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

          E-match theorems and case-splits performed by grind. Note that it may contain elements that are not needed by the final proof. For example, grind instantiated the theorem, but theorem instance was not actually used in the proof.

          Instances For
            Equations
            Instances For

              State for the GrindM monad.

              • ShareCommon (aka Hashconsing) state.

              • nextThmIdx : Nat

                Next index for creating auxiliary theorems.

              • Congruence theorems generated so far. Recall that for constant symbols we rely on the reserved name feature (i.e., mkHCongrWithArityForConst?). Remark: we currently do not reuse congruence theorems

              • simpStats : Simp.Stats
              • trueExpr : Expr
              • falseExpr : Expr
              • natZExpr : Expr
              • btrueExpr : Expr
              • bfalseExpr : Expr
              • lastTag : Name

                Used to generate trace messages of the for [grind] working on <tag>, and implement the macro trace_goal.

              • issues : List MessageData

                Issues found during the proof search. These issues are reported to users when grind fails.

              • trace : Trace

                trace for grind?

              • counters : Counters

                Performance counters

              Instances For

                Returns the user-defined configuration options

                Equations
                Instances For

                  Returns the internalized True constant.

                  Equations
                  Instances For

                    Returns the internalized False constant.

                    Equations
                    Instances For

                      Returns the internalized Bool.true.

                      Equations
                      Instances For

                        Returns the internalized Bool.false.

                        Equations
                        Instances For

                          Returns the internalized 0 : Nat numeral.

                          Equations
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Lean.Meta.Grind.saveCases (declName : Name) (eager : Bool) :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Returns maximum term generation that is considered during ematching.

                                Equations
                                Instances For

                                  Abtracts nested proofs in e. This is a preprocessing step performed before internalization.

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

                                    Applies hash-consing to e. Recall that all expressions in a grind goal have been hash-consed. We perform this step before we internalize expressions.

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

                                      Returns true if e is the internalized True expression.

                                      Equations
                                      Instances For

                                        Returns true if e is the internalized False expression.

                                        Equations
                                        Instances For

                                          Creates a congruence theorem for a f-applications with numArgs arguments.

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

                                                Stores information for a node in the egraph. Each internalized expression e has an ENode associated with it.

                                                • self : Expr

                                                  Node represented by this ENode.

                                                • next : Expr

                                                  Next element in the equivalence class.

                                                • root : Expr

                                                  Root (aka canonical representative) of the equivalence class

                                                • congr : Expr

                                                  congr is the term self is congruent to. We say self is the congruence class root if isSameExpr congr self. This field is initialized to self even if e is not an application.

                                                • target? : Option Expr

                                                  When e was added to this equivalence class because of an equality h : e = target, then we store target here, and h at proof?.

                                                • proof? : Option Expr
                                                • flipped : Bool

                                                  Proof has been flipped.

                                                • size : Nat

                                                  Number of elements in the equivalence class, this field is meaningless if node is not the root.

                                                • interpreted : Bool

                                                  interpreted := true if node should be viewed as an abstract value.

                                                • ctor : Bool

                                                  ctor := true if the head symbol is a constructor application.

                                                • hasLambdas : Bool

                                                  hasLambdas := true if the equivalence class contains lambda expressions.

                                                • heqProofs : Bool

                                                  If heqProofs := true, then some proofs in the equivalence class are based on heterogeneous equality.

                                                • idx : Nat

                                                  Unique index used for pretty printing and debugging purposes.

                                                • generation : Nat

                                                  The generation in which this enode was created.

                                                • mt : Nat

                                                  Modification time

                                                • offset? : Option Expr

                                                  The offset? field is used to propagate equalities from the grind congruence closure module to the offset constraints module. When grind merges two equivalence classes, and both have an associated offset? set to some e, the equality is propagated. This field is assigned during the internalization of offset terms.

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

                                                  New equality to be processed.

                                                  Instances For
                                                    structure Lean.Meta.Grind.CongrKey (enodes : ENodeMap) :

                                                    Key for the congruence table. We need access to the enodes to be able to retrieve the equivalence class roots.

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

                                                            Returns true if a and b are congruent modulo the equivalence classes in enodes.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              def Lean.Meta.Grind.isCongruent.goEq (enodes : ENodeMap) (lhs₁ rhs₁ lhs₂ rhs₂ : Expr) :
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                partial def Lean.Meta.Grind.isCongruent.go (enodes : ENodeMap) (a b : Expr) :
                                                                Equations
                                                                @[reducible, inline]
                                                                Equations
                                                                Instances For

                                                                  The E-matching module instantiates theorems using the EMatchTheorem proof and a (partial) assignment. We want to avoid instantiating the same theorem with the same assignment more than once. Therefore, we store the (pre-)instance information in set. Recall that the proofs of activated theorems have been hash-consed. The assignment contains internalized expressions, which have also been hash-consed.

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

                                                                    New fact to be processed.

                                                                    Instances For

                                                                      Canonicalizer state. See Canon.lean for additional details.

                                                                      Instances For

                                                                        Trace information for a case split.

                                                                        Instances For
                                                                          • mvarId : MVarId
                                                                          • canon : Canon.State
                                                                          • enodes : ENodeMap
                                                                          • parents : ParentMap
                                                                          • congrTable : CongrTable self.enodes
                                                                          • A mapping from each function application index (HeadIndex) to a list of applications with that index. Recall that the HeadIndex for a constant is its constant name, and for a free variable, it is its unique id.

                                                                          • newEqs : Array NewEq

                                                                            Equations to be processed.

                                                                          • inconsistent : Bool

                                                                            inconsistent := true if ENodes for True and False are in the same equivalence class.

                                                                          • gmt : Nat

                                                                            Goal modification time.

                                                                          • nextIdx : Nat

                                                                            Next unique index for creating ENodes

                                                                          • arith : Arith.State

                                                                            State of arithmetic procedures

                                                                          • casesTypes : CasesTypes

                                                                            Inductive datatypes marked for case-splitting

                                                                          • Active theorems that we have performed ematching at least once.

                                                                          • Active theorems that we have not performed any round of ematching yet.

                                                                          • Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols. Local theorem provided by users are added directly into newThms.

                                                                          • numInstances : Nat

                                                                            Number of theorem instances generated so far

                                                                          • numEmatch : Nat

                                                                            Number of E-matching rounds performed in this goal since the last case-split.

                                                                          • preInstances : PreInstanceSet

                                                                            (pre-)instances found so far. It includes instances that failed to be instantiated.

                                                                          • newFacts : Std.Queue NewFact

                                                                            new facts to be processed.

                                                                          • matchEqNames : PHashSet Name

                                                                            match auxiliary functions whose equations have already been created and activated.

                                                                          • splitCandidates : List Expr

                                                                            Case-split candidates.

                                                                          • numSplits : Nat

                                                                            Number of splits performed to get to this goal.

                                                                          • resolvedSplits : PHashSet ENodeKey

                                                                            Case-splits that have already been performed, or that do not have to be performed anymore.

                                                                          • nextThmIdx : Nat

                                                                            Next local E-match theorem idx.

                                                                          • facts : PArray Expr

                                                                            Asserted facts

                                                                          • Cached extensionality theorems for types.

                                                                          • casesTrace : List CaseTrace

                                                                            Sequence of cases steps that generated this goal. We only use this information for diagnostics. Remark: casesTrace.length ≥ numSplits because we don't increase the counter for cases applications that generated only 1 subgoal.

                                                                          Instances For
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def Lean.Meta.Grind.GoalM.run {α : Type} (goal : Goal) (x : GoalM α) :
                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                Equations
                                                                                Instances For
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For

                                                                                    Macro similar to trace[...], but it includes the trace message trace[grind] "working on <current goal>" if the tag has changed since the last trace message.

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

                                                                                      A helper function used to mark a theorem instance found by the E-matching module. It returns true if it is a new instance and false otherwise.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        def Lean.Meta.Grind.addNewFact (proof prop : Expr) (generation : Nat) :

                                                                                        Adds a new fact prop with proof proof to the queue for processing.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          def Lean.Meta.Grind.addTheoremInstance (thm : EMatchTheorem) (proof prop : Expr) (generation : Nat) :

                                                                                          Adds a new theorem instance produced using E-matching.

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

                                                                                            Returns true if the maximum number of instances has been reached.

                                                                                            Equations
                                                                                            Instances For

                                                                                              Returns true if the maximum number of case-splits has been reached.

                                                                                              Equations
                                                                                              Instances For

                                                                                                Returns true if the maximum number of E-matching rounds has been reached.

                                                                                                Equations
                                                                                                Instances For

                                                                                                  Returns some n if e has already been "internalized" into the Otherwise, returns nones.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[inline]

                                                                                                    Returns some n if e has already been "internalized" into the Otherwise, returns nones.

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

                                                                                                        Returns node associated with e. It assumes e has already been internalized.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[inline]

                                                                                                          Returns node associated with e. It assumes e has already been internalized.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            Returns the generation of the given term. Is assumes it has been internalized

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Returns true if e is in the equivalence class of True.

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                Returns true if e is in the equivalence class of False.

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  Returns true if e is in the equivalence class of Bool.true.

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

                                                                                                                    Returns true if e is in the equivalence class of Bool.false.

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

                                                                                                                      Returns true if a and b are in the same equivalence class.

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

                                                                                                                        Returns true if the root of its equivalence class.

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          Returns the root element in the equivalence class of e IF e has been internalized.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[inline]

                                                                                                                            Returns the root element in the equivalence class of e IF e has been internalized.

                                                                                                                            Equations
                                                                                                                            Instances For

                                                                                                                              Returns the root element in the equivalence class of e.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                @[inline]

                                                                                                                                Returns the root element in the equivalence class of e.

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  Returns the root enode in the equivalence class of e.

                                                                                                                                  Equations
                                                                                                                                  Instances For

                                                                                                                                    Returns the root enode in the equivalence class of e if it is in an equivalence class.

                                                                                                                                    Equations
                                                                                                                                    Instances For

                                                                                                                                      Returns the next element in the equivalence class of e if e has been internalized in the given goal.

                                                                                                                                      Equations
                                                                                                                                      Instances For

                                                                                                                                        Returns the next element in the equivalence class of e.

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[inline]

                                                                                                                                          Returns the root element in the equivalence class of e.

                                                                                                                                          Equations
                                                                                                                                          Instances For

                                                                                                                                            Returns true if e has already been internalized.

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  def Lean.Meta.Grind.pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) :

                                                                                                                                                  If isHEq is false, it pushes lhs = rhs with proof to newEqs. Otherwise, it pushes HEq lhs rhs.

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

                                                                                                                                                    Return true if a and b have the same type.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      def Lean.Meta.Grind.pushEqHEq (lhs rhs proof : Expr) :
                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        def Lean.Meta.Grind.pushEq (lhs rhs proof : Expr) :

                                                                                                                                                        Pushes lhs = rhs with proof to newEqs.

                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def Lean.Meta.Grind.pushHEq (lhs rhs proof : Expr) :

                                                                                                                                                          Pushes HEq lhs rhs with proof to newEqs.

                                                                                                                                                          Equations
                                                                                                                                                          Instances For

                                                                                                                                                            Pushes a = True with proof to newEqs.

                                                                                                                                                            Equations
                                                                                                                                                            Instances For

                                                                                                                                                              Pushes a = False with proof to newEqs.

                                                                                                                                                              Equations
                                                                                                                                                              Instances For

                                                                                                                                                                Pushes a = Bool.true with proof to newEqs.

                                                                                                                                                                Equations
                                                                                                                                                                Instances For

                                                                                                                                                                  Pushes a = Bool.false with proof to newEqs.

                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For

                                                                                                                                                                    Records that parent is a parent of child. This function actually stores the information in the root (aka canonical representative) of child.

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

                                                                                                                                                                      Returns the set of expressions e is a child of, or an expression in es equivalence class is a child of. The information is only up to date if e is the root (aka canonical representative) of the equivalence class.

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For

                                                                                                                                                                        Removes the entry eparents from the parent map.

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

                                                                                                                                                                          Copy parents to the parents of root. root must be the root of its equivalence class.

                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            Equations
                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                            Instances For
                                                                                                                                                                              def Lean.Meta.Grind.mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) :
                                                                                                                                                                              Equations
                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                              Instances For
                                                                                                                                                                                def Lean.Meta.Grind.mkENode (e : Expr) (generation : Nat) :

                                                                                                                                                                                Creates an ENode for e if one does not already exist. This method assumes e has been hashconsed.

                                                                                                                                                                                Equations
                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[extern lean_process_new_offset_eq]

                                                                                                                                                                                  Notify the offset constraint module that a = b where a and b are terms that have been internalized by this module.

                                                                                                                                                                                  @[extern lean_process_new_offset_eq_lit]

                                                                                                                                                                                  Notify the offset constraint module that a = k where a is term that has been internalized by this module, and k is a numeral.

                                                                                                                                                                                  Returns true if e is a numeral and has type Nat.

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

                                                                                                                                                                                    Marks e as a term of interest to the offset constraint module. If the root of es equivalence class has already a term of interest, a new equality is propagated to the offset module.

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

                                                                                                                                                                                      Returns true is e is the root of its congruence class.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For

                                                                                                                                                                                        Returns the root of the congruence class containing e.

                                                                                                                                                                                        Return true if the goal is inconsistent.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[extern lean_grind_mk_eq_proof]

                                                                                                                                                                                          Returns a proof that a = b. It assumes a and b are in the same equivalence class, and have the same type.

                                                                                                                                                                                          @[extern lean_grind_mk_heq_proof]

                                                                                                                                                                                          Returns a proof that HEq a b. It assumes a and b are in the same equivalence class.

                                                                                                                                                                                          @[extern lean_grind_internalize]
                                                                                                                                                                                          opaque Lean.Meta.Grind.internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) :
                                                                                                                                                                                          @[extern lean_grind_process_new_eqs]

                                                                                                                                                                                          Returns a proof that a = b if they have the same type. Otherwise, returns a proof of HEq a b. It assumes a and b are in the same equivalence class.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For

                                                                                                                                                                                            Returns a proof that a = True. It assumes a and True are in the same equivalence class.

                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For

                                                                                                                                                                                              Returns a proof that a = False. It assumes a and False are in the same equivalence class.

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                Returns a proof that a = Bool.true. It assumes a and Bool.true are in the same equivalence class.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  Returns a proof that a = Bool.false. It assumes a and Bool.false are in the same equivalence class.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                    Marks current goal as inconsistent without assigning mvarId.

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

                                                                                                                                                                                                      Closes the current goal using the given proof of False and marks it as inconsistent if it is not already marked so.

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

                                                                                                                                                                                                          Returns all enodes in the goal

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            @[inline]

                                                                                                                                                                                                            Executes f to each term in the equivalence class containing e

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                              def Lean.Meta.Grind.foldEqc {α : Type} (e : Expr) (init : α) (f : ENodeαGoalM α) :

                                                                                                                                                                                                              Folds using f and init over the equivalence class containing e

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

                                                                                                                                                                                                                          Returns expressions in the given expression equivalence class.

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            partial def Lean.Meta.Grind.Goal.getEqc.go (goal : Goal) (first e : Expr) (acc : List Expr) :
                                                                                                                                                                                                                            @[inline]

                                                                                                                                                                                                                            Returns expressions in the given expression equivalence class.

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                              Returns all equivalence classes in the current goal.

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                @[inline]

                                                                                                                                                                                                                                Returns all equivalence classes in the current goal.

                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                  Returns true if e is a case-split that does not need to be performed anymore.

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                    Mark e as a case-split that does not need to be performed anymore. Remark: we currently use this feature to disable match-case-splits. Remark: we also use this feature to record the case-splits that have already been performed.

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

                                                                                                                                                                                                                                      Returns extensionality theorems for the given type if available. If Config.ext is false, the result is #[].

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

                                                                                                                                                                                                                                        Helper function for instantiating a type class type, and then using the result to perform isDefEq x val.

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