Documentation

Lean.Util.Recognizers

@[inline]
Equations
Instances For
    @[inline]
    Equations
    • e.app1? fName = if e.isAppOfArity fName 1 = true then some e.appArg! else none
    Instances For
      @[inline]
      Equations
      • e.app2? fName = if e.isAppOfArity fName 2 = true then some (e.appFn!.appArg!, e.appArg!) else none
      Instances For
        @[inline]
        Equations
        • e.app3? fName = if e.isAppOfArity fName 3 = true then some (e.appFn!.appFn!.appArg!, e.appFn!.appArg!, e.appArg!) else none
        Instances For
          @[inline]
          Equations
          • e.app4? fName = if e.isAppOfArity fName 4 = true then some (e.appFn!.appFn!.appFn!.appArg!, e.appFn!.appFn!.appArg!, e.appFn!.appArg!, e.appArg!) else none
          Instances For
            @[inline]
            Equations
            • p.eq? = p.app3? `Eq
            Instances For
              @[inline]
              Equations
              • p.ne? = p.app3? `Ne
              Instances For
                @[inline]
                Equations
                • p.iff? = p.app2? `Iff
                Instances For
                  @[inline]
                  Equations
                  • p.eqOrIff? = match p.app3? `Eq with | some (fst, lhs, rhs) => some (lhs, rhs) | x => p.iff?
                  Instances For
                    @[inline]
                    Equations
                    • p.not? = p.app1? `Not
                    Instances For
                      @[inline]
                      Equations
                      • p.notNot? = match p.not? with | some p => p.not? | none => none
                      Instances For
                        @[inline]
                        Equations
                        • p.and? = p.app2? `And
                        Instances For
                          @[inline]
                          Equations
                          • p.heq? = p.app4? `HEq
                          Instances For
                            Equations
                            • e.natAdd? = e.app2? `Nat.add
                            Instances For
                              @[inline]
                              Equations
                              Instances For
                                Equations
                                • e.isEq = e.isAppOfArity `Eq 3
                                Instances For
                                  Equations
                                  • e.isHEq = e.isAppOfArity `HEq 4
                                  Instances For
                                    Equations
                                    • e.isIte = e.isAppOfArity `ite 5
                                    Instances For
                                      Equations
                                      • e.isDIte = e.isAppOfArity `dite 5
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          • e.arrayLit? = if e.isAppOfArity' `List.toArray 2 = true then e.appArg!'.listLit? else none
                                          Instances For

                                            Recognize α × β

                                            Equations
                                            • e.prod? = e.app2? `Prod
                                            Instances For