Documentation

MeTTaILProofs.DecEq

DottedPath (no nesting) #

source
instance MeTTaIL.instReflBEqDottedPath_meTTaILProofs :
ReflBEq DottedPath
source
instance MeTTaIL.instLawfulBEqDottedPath_meTTaILProofs :
LawfulBEq DottedPath
source
@[implicit_reducible]
instance MeTTaIL.instDecidableEqDottedPath_meTTaILProofs :
DecidableEq DottedPath
Equations
source
def MeTTaIL.instDecidableEqDottedPath_meTTaILProofs.decEq (x✝ x✝¹ : DottedPath) :
Decidable (x✝ = x✝¹)
Equations
Instances For

    Cat (nests through prod : List Cat) #

    source
    theorem MeTTaIL.Cat.beq_refl (a : Cat) :
    a.beq a = true

    Cat.beq is reflexive.

    source
    theorem MeTTaIL.Cat.beqList_refl (cs : List Cat) :
    beqList cs cs = true

    Cat.beqList is reflexive.

    source
    theorem MeTTaIL.Cat.eq_of_beq {a b : Cat} :
    a.beq b = true → a = b

    Cat.beq a b = true implies a = b.

    source
    theorem MeTTaIL.Cat.beqList_eq {cs ds : List Cat} :
    beqList cs ds = true → cs = ds

    Cat.beqList cs ds = true implies cs = ds.

    source
    instance MeTTaIL.instLawfulBEqCat_meTTaILProofs :
    LawfulBEq Cat
    source
    @[implicit_reducible]
    instance MeTTaIL.instDecidableEqCat_meTTaILProofs :
    DecidableEq Cat
    Equations

    Label, Item, Rule (mention Cat, no List nesting of themselves) #

    source
    instance MeTTaIL.instReflBEqLabel_meTTaILProofs :
    ReflBEq Label
    source
    instance MeTTaIL.instLawfulBEqLabel_meTTaILProofs :
    LawfulBEq Label
    source
    def MeTTaIL.instDecidableEqLabel_meTTaILProofs.decEq (x✝ x✝¹ : Label) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance MeTTaIL.instDecidableEqLabel_meTTaILProofs :
      DecidableEq Label
      Equations
      source
      instance MeTTaIL.instReflBEqItem_meTTaILProofs :
      ReflBEq Item
      source
      instance MeTTaIL.instLawfulBEqItem_meTTaILProofs :
      LawfulBEq Item
      source
      def MeTTaIL.instDecidableEqItem_meTTaILProofs.decEq (x✝ x✝¹ : Item) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance MeTTaIL.instDecidableEqItem_meTTaILProofs :
        DecidableEq Item
        Equations
        source
        instance MeTTaIL.instReflBEqRule_meTTaILProofs :
        ReflBEq Rule
        source
        instance MeTTaIL.instLawfulBEqRule_meTTaILProofs :
        LawfulBEq Rule
        source
        @[implicit_reducible]
        instance MeTTaIL.instDecidableEqRule_meTTaILProofs :
        DecidableEq Rule
        Equations
        source
        def MeTTaIL.instDecidableEqRule_meTTaILProofs.decEq (x✝ x✝¹ : Rule) :
        Decidable (x✝ = x✝¹)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          AST (nests through sexp ... : List AST) #

          source
          theorem MeTTaIL.AST.beq_refl (a : AST) :
          a.beq a = true

          AST.beq is reflexive.

          source
          theorem MeTTaIL.AST.beqList_refl (cs : List AST) :
          beqList cs cs = true

          AST.beqList is reflexive.

          source
          theorem MeTTaIL.AST.eq_of_beq {a b : AST} :
          a.beq b = true → a = b

          AST.beq a b = true implies a = b.

          source
          theorem MeTTaIL.AST.beqList_eq {cs ds : List AST} :
          beqList cs ds = true → cs = ds

          AST.beqList cs ds = true implies cs = ds.

          source
          instance MeTTaIL.instLawfulBEqAST_meTTaILProofs :
          LawfulBEq AST
          source
          @[implicit_reducible]
          instance MeTTaIL.instDecidableEqAST_meTTaILProofs :
          DecidableEq AST
          Equations

          Equation, Hyp, Rewrite, RewriteDecl (mention AST / DottedPath) #

          source
          instance MeTTaIL.instReflBEqEquation_meTTaILProofs :
          ReflBEq Equation
          source
          instance MeTTaIL.instLawfulBEqEquation_meTTaILProofs :
          LawfulBEq Equation
          source
          @[implicit_reducible]
          instance MeTTaIL.instDecidableEqEquation_meTTaILProofs :
          DecidableEq Equation
          Equations
          source
          def MeTTaIL.instDecidableEqEquation_meTTaILProofs.decEq (x✝ x✝¹ : Equation) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            instance MeTTaIL.instReflBEqHyp_meTTaILProofs :
            ReflBEq Hyp
            source
            instance MeTTaIL.instLawfulBEqHyp_meTTaILProofs :
            LawfulBEq Hyp
            source
            def MeTTaIL.instDecidableEqHyp_meTTaILProofs.decEq (x✝ x✝¹ : Hyp) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              source
              @[implicit_reducible]
              instance MeTTaIL.instDecidableEqHyp_meTTaILProofs :
              DecidableEq Hyp
              Equations
              source
              instance MeTTaIL.instReflBEqRewrite_meTTaILProofs :
              ReflBEq Rewrite
              source
              instance MeTTaIL.instLawfulBEqRewrite_meTTaILProofs :
              LawfulBEq Rewrite
              source
              @[implicit_reducible]
              instance MeTTaIL.instDecidableEqRewrite_meTTaILProofs :
              DecidableEq Rewrite
              Equations
              source
              def MeTTaIL.instDecidableEqRewrite_meTTaILProofs.decEq (x✝ x✝¹ : Rewrite) :
              Decidable (x✝ = x✝¹)
              Equations
              Instances For
                source
                instance MeTTaIL.instReflBEqRewriteDecl_meTTaILProofs :
                ReflBEq RewriteDecl
                source
                instance MeTTaIL.instLawfulBEqRewriteDecl_meTTaILProofs :
                LawfulBEq RewriteDecl
                source
                def MeTTaIL.instDecidableEqRewriteDecl_meTTaILProofs.decEq (x✝ x✝¹ : RewriteDecl) :
                Decidable (x✝ = x✝¹)
                Equations
                Instances For
                  source
                  @[implicit_reducible]
                  instance MeTTaIL.instDecidableEqRewriteDecl_meTTaILProofs :
                  DecidableEq RewriteDecl
                  Equations

                  Presentation (nests through references : List (String × Presentation)) #

                  source
                  theorem MeTTaIL.Presentation.beq_refl (p : Presentation) :
                  p.beq p = true

                  Presentation.beq is reflexive.

                  source
                  theorem MeTTaIL.Presentation.beqRefs_refl (m : List (String × Presentation)) :
                  beqRefs m m = true

                  Presentation.beqRefs is reflexive.

                  source
                  theorem MeTTaIL.Presentation.eq_of_beq {p q : Presentation} :
                  p.beq q = true → p = q

                  Presentation.beq p q = true implies p = q.

                  source
                  theorem MeTTaIL.Presentation.beqRefs_eq {m₁ m₂ : List (String × Presentation)} :
                  beqRefs m₁ m₂ = true → m₁ = m₂

                  Presentation.beqRefs m₁ m₂ = true implies m₁ = m₂.

                  source
                  instance MeTTaIL.instLawfulBEqPresentation_meTTaILProofs :
                  LawfulBEq Presentation
                  source
                  @[implicit_reducible]
                  instance MeTTaIL.instDecidableEqPresentation_meTTaILProofs :
                  DecidableEq Presentation
                  Equations