mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 02:07:25 +03:00
[ refactoring ] Tiny changes following up the idris-lang/Idris2#830
Some zeroes in signatures, one simpler implementation and formatting.
This commit is contained in:
parent
e58bcfc7ef
commit
8038f0a0f9
@ -229,7 +229,7 @@ namespace Equality
|
||||
|
||||
||| The actual proof used by cast is irrelevant
|
||||
export
|
||||
congCast : {n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
|
||||
congCast : {0 n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
|
||||
{0 eq1 : m = n} -> {0 eq2 : p = q} ->
|
||||
k ~~~ l ->
|
||||
cast eq1 k ~~~ cast eq2 l
|
||||
@ -237,9 +237,8 @@ namespace Equality
|
||||
|
||||
||| Last is congruent wrt index equality
|
||||
export
|
||||
congLast : {m, n : Nat} -> (0 _ : m = n) -> last {n=m} ~~~ last {n}
|
||||
congLast {m = Z} {n = Z} eq = reflexive
|
||||
congLast {m = S _} {n = S _} eq = FS (congLast (succInjective _ _ eq))
|
||||
congLast : {m : Nat} -> (0 _ : m = n) -> last {n=m} ~~~ last {n}
|
||||
congLast Refl = reflexive
|
||||
|
||||
export
|
||||
congShift : (m : Nat) -> k ~~~ l -> shift m k ~~~ shift m l
|
||||
@ -263,7 +262,7 @@ namespace Equality
|
||||
export
|
||||
hetPointwiseIsTransport :
|
||||
{0 k : Fin m} -> {0 l : Fin n} ->
|
||||
(eq : m === n) -> k ~~~ l -> k === rewrite eq in l
|
||||
(0 eq : m === n) -> k ~~~ l -> k === rewrite eq in l
|
||||
hetPointwiseIsTransport Refl = homoPointwiseIsEqual
|
||||
|
||||
export
|
||||
|
@ -213,7 +213,7 @@ finToNatMultHomo {m = S _} (FS x) y = Calc $
|
||||
~~ finToNat (y + x * y) ...( Refl )
|
||||
~~ finToNat y + finToNat (x * y) ...( finToNatPlusHomo y (x * y) )
|
||||
~~ finToNat y + finToNat x * finToNat y ...( cong (finToNat y +) (finToNatMultHomo x y) )
|
||||
~~ finToNat (FS x) * finToNat y ...( Refl)
|
||||
~~ finToNat (FS x) * finToNat y ...( Refl )
|
||||
|
||||
-- Relations to `Fin`'s `last`
|
||||
|
||||
@ -292,7 +292,7 @@ plusZeroRightNeutral (FS k) = FS (plusZeroRightNeutral k)
|
||||
|
||||
export
|
||||
congPlusRight : {m, n, p : Nat} -> {k : Fin (S n)} -> {l : Fin (S p)} ->
|
||||
(c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
|
||||
(c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
|
||||
congPlusRight c FZ
|
||||
= transitive (plusZeroRightNeutral c)
|
||||
(symmetric $ plusZeroRightNeutral c)
|
||||
|
Loading…
Reference in New Issue
Block a user