Documentation

Aesop.Util.EqualUpToIds

  • allowAssignmentDiff : Bool

    Allow metavariables to be unassigned on one side of the comparison and assigned on the other. So when we compare two expressions and we encounter a metavariable ?x in one of them and a subexpression e in the other (at the same position), we consider ?x equal to e.

Instances For
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Aesop.EqualUpToIdsM.run {α : Type} (x : Aesop.EqualUpToIdsM α) (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (allowAssignmentDiff : Bool) :
        Equations
        • x.run commonMCtx? mctx₁ mctx₂ allowAssignmentDiff = (fun (x : α × Aesop.EqualUpToIdsM.State) => x.fst) <$> x.run' commonMCtx? mctx₁ mctx₂ allowAssignmentDiff
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                Equations
                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
                        @[implemented_by Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore]
                        @[implemented_by Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore]
                        @[implemented_by Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore]
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Aesop.exprsEqualUpToIds (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (lctx₁ : Lean.LocalContext) (lctx₂ : Lean.LocalContext) (localInstances₁ : Lean.LocalInstances) (localInstances₂ : Lean.LocalInstances) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (allowAssignmentDiff : optParam Bool false) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Aesop.exprsEqualUpToIds' (e₁ : Lean.Expr) (e₂ : Lean.Expr) (allowAssignmentDiff : optParam Bool false) :
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Aesop.unassignedMVarsEqualUptoIds (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (mvarId₁ : Lean.MVarId) (mvarId₂ : Lean.MVarId) (allowAssignmentDiff : optParam Bool false) :
                              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 Aesop.tacticStatesEqualUpToIds (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (goals₁ : Array Lean.MVarId) (goals₂ : Array Lean.MVarId) (allowAssignmentDiff : optParam Bool false) :
                                  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