Documentation

Init.Data.Fin.Basic

instance Fin.coeToNat {n : Nat} :
Equations
  • Fin.coeToNat = { coe := fun v => v.val }
def Fin.elim0 {α : Sort u} :
Fin 0α
Equations
Instances For
    def Fin.succ {n : Nat} :
    Fin nFin (Nat.succ n)
    Equations
    Instances For
      def Fin.ofNat {n : Nat} (a : Nat) :
      Equations
      Instances For
        def Fin.ofNat' {n : Nat} (a : Nat) (h : n > 0) :
        Fin n
        Equations
        Instances For
          def Fin.add {n : Nat} :
          Fin nFin nFin n
          Equations
          • Fin.add x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + b) % n, isLt := (_ : (a + b) % n < n) }
          Instances For
            def Fin.mul {n : Nat} :
            Fin nFin nFin n
            Equations
            • Fin.mul x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a * b % n, isLt := (_ : a * b % n < n) }
            Instances For
              def Fin.sub {n : Nat} :
              Fin nFin nFin n
              Equations
              • Fin.sub x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + (n - b)) % n, isLt := (_ : (a + (n - b)) % n < n) }
              Instances For

                Remark: mod/div/modn/land/lor can be defined without using (% n), but we are trying to minimize the number of Nat theorems needed to boostrap Lean.

                def Fin.mod {n : Nat} :
                Fin nFin nFin n
                Equations
                • Fin.mod x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a % b % n, isLt := (_ : a % b % n < n) }
                Instances For
                  def Fin.div {n : Nat} :
                  Fin nFin nFin n
                  Equations
                  • Fin.div x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a / b % n, isLt := (_ : a / b % n < n) }
                  Instances For
                    def Fin.modn {n : Nat} :
                    Fin nNatFin n
                    Equations
                    • Fin.modn x x = match x, x with | { val := a, isLt := h }, m => { val := a % m % n, isLt := (_ : a % m % n < n) }
                    Instances For
                      def Fin.land {n : Nat} :
                      Fin nFin nFin n
                      Equations
                      • Fin.land x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.land a b % n, isLt := (_ : Nat.land a b % n < n) }
                      Instances For
                        def Fin.lor {n : Nat} :
                        Fin nFin nFin n
                        Equations
                        • Fin.lor x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.lor a b % n, isLt := (_ : Nat.lor a b % n < n) }
                        Instances For
                          def Fin.xor {n : Nat} :
                          Fin nFin nFin n
                          Equations
                          • Fin.xor x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.xor a b % n, isLt := (_ : Nat.xor a b % n < n) }
                          Instances For
                            def Fin.shiftLeft {n : Nat} :
                            Fin nFin nFin n
                            Equations
                            • Fin.shiftLeft x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a <<< b % n, isLt := (_ : a <<< b % n < n) }
                            Instances For
                              def Fin.shiftRight {n : Nat} :
                              Fin nFin nFin n
                              Equations
                              • Fin.shiftRight x x = match x, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a >>> b % n, isLt := (_ : a >>> b % n < n) }
                              Instances For
                                instance Fin.instAddFin {n : Nat} :
                                Add (Fin n)
                                Equations
                                • Fin.instAddFin = { add := Fin.add }
                                instance Fin.instSubFin {n : Nat} :
                                Sub (Fin n)
                                Equations
                                • Fin.instSubFin = { sub := Fin.sub }
                                instance Fin.instMulFin {n : Nat} :
                                Mul (Fin n)
                                Equations
                                • Fin.instMulFin = { mul := Fin.mul }
                                instance Fin.instModFin {n : Nat} :
                                Mod (Fin n)
                                Equations
                                • Fin.instModFin = { mod := Fin.mod }
                                instance Fin.instDivFin {n : Nat} :
                                Div (Fin n)
                                Equations
                                • Fin.instDivFin = { div := Fin.div }
                                instance Fin.instAndOpFin {n : Nat} :
                                Equations
                                • Fin.instAndOpFin = { and := Fin.land }
                                instance Fin.instOrOpFin {n : Nat} :
                                OrOp (Fin n)
                                Equations
                                • Fin.instOrOpFin = { or := Fin.lor }
                                instance Fin.instXorFin {n : Nat} :
                                Xor (Fin n)
                                Equations
                                • Fin.instXorFin = { xor := Fin.xor }
                                Equations
                                • Fin.instShiftLeftFin = { shiftLeft := Fin.shiftLeft }
                                Equations
                                • Fin.instShiftRightFin = { shiftRight := Fin.shiftRight }
                                Equations
                                • Fin.instOfNatFinHAddNatInstHAddInstAddNatOfNat = { ofNat := Fin.ofNat i }
                                Equations
                                • Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat = { default := 0 }
                                theorem Fin.val_ne_of_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i j) :
                                i.val j.val
                                theorem Fin.modn_lt {n : Nat} {m : Nat} (i : Fin n) :
                                m > 0(Fin.modn i m).val < m
                                theorem Fin.val_lt_of_le {n : Nat} {b : Nat} (i : Fin b) (h : b n) :
                                i.val < n
                                instance instGetElemFinVal {cont : Type u_1} {elem : Type u_2} {dom : contNatProp} {n : Nat} [GetElem cont Nat elem dom] :
                                GetElem cont (Fin n) elem fun xs i => dom xs i.val
                                Equations
                                • instGetElemFinVal = { getElem := fun xs i h => xs[i.val] }