Equations
-
Fin.coeToNat = { coe := fun v => v.val }
Equations
-
Fin.elim0 _fun_discr = match _fun_discr with
| { val := val, isLt := h } => absurd h (_ : ¬val < 0)
Equations
-
Fin.add _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + b) % n, isLt := (_ : (a + b) % n < n) }
Equations
-
Fin.mul _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a * b % n, isLt := (_ : a * b % n < n) }
Equations
-
Fin.sub _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } =>
{ val := (a + (n - b)) % n, isLt := (_ : (a + (n - b)) % n < n) }
Equations
-
Fin.mod _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a % b % n, isLt := (_ : a % b % n < n) }
Equations
-
Fin.div _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a / b % n, isLt := (_ : a / b % n < n) }
Equations
-
Fin.modn _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, m => { val := a % m % n, isLt := (_ : a % m % n < n) }
Equations
-
Fin.land _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } =>
{ val := Nat.land a b % n, isLt := (_ : Nat.land a b % n < n) }
Equations
-
Fin.lor _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.lor a b % n, isLt := (_ : Nat.lor a b % n < n) }
Equations
-
Fin.xor _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.xor a b % n, isLt := (_ : Nat.xor a b % n < n) }
Equations
-
Fin.shiftLeft _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a <<< b % n, isLt := (_ : a <<< b % n < n) }
Equations
-
Fin.shiftRight _fun_discr _fun_discr = match _fun_discr, _fun_discr with
| { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a >>> b % n, isLt := (_ : a >>> b % n < n) }
Equations
-
Fin.instAddFin = { add := Fin.add }
Equations
-
Fin.instSubFin = { sub := Fin.sub }
Equations
-
Fin.instMulFin = { mul := Fin.mul }
Equations
-
Fin.instModFin = { mod := Fin.mod }
Equations
-
Fin.instDivFin = { div := Fin.div }
Equations
-
Fin.instAndOpFin = { and := Fin.land }
Equations
-
Fin.instOrOpFin = { or := Fin.lor }
Equations
-
Fin.instXorFin = { xor := Fin.xor }
Equations
-
Fin.instShiftLeftFin = { shiftLeft := Fin.shiftLeft }
Equations
-
Fin.instShiftRightFin = { shiftRight := Fin.shiftRight }
Equations
-
Fin.instHModFinNat = { hMod := Fin.modn }
Equations
-
Fin.instOfNatFinHAddNatInstHAddInstAddNatOfNat = { ofNat := Fin.ofNat i }
Equations
-
Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat = { default := 0 }