insert_perm a is a permutation of fin2 n with the following properties:
insert_perm a i = i+1ifi < ainsert_perm a a = 0insert_perm a i = iifi > a
remap_left f k : fin2 (m + k) → fin2 (n + k) applies the function
f : fin2 m → fin2 n to inputs less than m, and leaves the right part
on the right (that is, remap_left f k (m + i) = n + i).
Equations
- fin2.remap_left f k.succ i.fs = (fin2.remap_left f k i).fs
- fin2.remap_left f k.succ fin2.fz = fin2.fz
- fin2.remap_left f 0 i = f i
@[class]
- h : m < n
This is a simple type class inference prover for proof obligations
of the form m < n where m n : ℕ.
Instances
@[instance]
Equations
- fin2.is_lt.zero n = {h := _}
@[instance]
Equations
- fin2.is_lt.succ m n = {h := _}
Use type class inference to infer the boundedness proof, so that we
can directly convert a nat into a fin2 n. This supports
notation like &1 : fin 3.
Equations
- fin2.of_nat' m.succ = (fin2.of_nat' m).fs
- fin2.of_nat' 0 = fin2.fz
- fin2.of_nat' m = absurd h _