# 甚至从模板发生的Idris类型不匹配

##### 问题描述投票：1回答：1

``````data ModEq : (n:Nat) -> (x:Nat) -> (y:Nat) -> Type where
{- 3 constructors
reflexive:      x == x (mod n),
left-induct:    x == y (mod n) => (x+n) == y    (mod n)
right-induct:   x == y (mod n) => x == (y+n)    (mod n)
-}
Reflex : (x:Nat) -> ModEq n x x  --- Needs syntatic sugar, for now prefix
LInd : (ModEq n x y) -> ModEq n (x+n) y
RInd : (ModEq n x y) -> ModEq n x (y+n)

{----- Proof of transitive property. -----}
total
isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
{- x=x & x=y => x=y -}
isTrans (Reflex x) v = v
isTrans u (Reflex y) = u
{- ((x=y=>(x+n)=y) & y=z) => x=y & y=z => x=z (induct) => (x+n)=z -}
isTrans (LInd u) v = LInd (isTrans u v)
isTrans u (RInd v) = RInd (isTrans u v)
{- (x=y=>x=(y+n)) & (y=z=>(y+n)=z) => x=y & y=z => x=z (induct) -}
isTrans (RInd u) (LInd v) = isTrans u v
``````

``````48 | isTrans (RInd u) (LInd v) = isTrans u v
| ~~~~~~~
When checking left hand side of isTrans:
When checking an application of Main.isTrans:
Type mismatch between
ModEq n (x + n) z (Type of LInd v)
and
ModEq n (y + n) z (Expected type)

Specifically:
Type mismatch between
plus x n
and
plus y n
``````

``````isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
isTrans (RInd _) (LInd _) = ?isTrans_rhs_1
``````

``````40 | isTrans (RInd _) (LInd _) = ?isTrans_rhs_1
| ~~~~~~~
When checking left hand side of isTrans:
When checking an application of Main.isTrans:
Type mismatch between
ModEq n (x + n) z (Type of LInd _)
and
ModEq n (y + n) z (Expected type)

Specifically:
Type mismatch between
plus x n
and
plus y n
``````
idris typechecking theorem-proving
##### 1个回答
2

``````isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
isTrans (Reflex _) v = v
isTrans u (Reflex _) = u
isTrans (LInd u) v = LInd \$ isTrans u v
isTrans u (RInd v) = RInd \$ isTrans u v
isTrans (RInd u) (LInd v) {n} {x} {y = x + n} = ?isTrans_rhs
``````

``````  x : Nat
n : Nat
u : ModEq n x x
z : Nat
v : ModEq n x z
--------------------------------------
isTrans_rhs : ModEq n x z
``````