mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-24 12:54:28 +03:00
5383bd89be
There was a check on evaluating lets which was in Blodwen but I hadn't added to the normaliser yet! Also, normalisation needs to reduce as patterns for unification, but not when reducing finished LHS and argument terms. This is a bit of a hack (but then, so is the implementation of as patterns in general...). So, when we're checking a nested expression, we have the as pattern as a let bound variable (so that it has the necessary computational force) but when we compile we just pass it as an ordinary argument, then it gets the desired behaviour in case trees.
41 lines
875 B
Plaintext
41 lines
875 B
Plaintext
data Nat : Type where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
plus : Nat -> Nat -> Nat
|
|
plus Z $y = y
|
|
plus (S $k) $y = S (plus k y)
|
|
|
|
cplus : Nat -> Nat -> Nat
|
|
cplus $x $y
|
|
= case x of
|
|
Z => y
|
|
S $k => S (cplus k y)
|
|
|
|
data Vect : Nat -> Type -> Type where
|
|
Nil : Vect Z $a
|
|
Cons : $a -> Vect $k $a -> Vect (S $k) $a
|
|
|
|
append : Vect $n $a -> Vect $m $a -> Vect (cplus $n $m) $a
|
|
append Nil $ys = ys
|
|
append (Cons $x $xs) $ys = Cons x (append xs ys)
|
|
|
|
cappend : Vect $n $a -> Vect $m $a -> Vect (cplus $n $m) $a
|
|
cappend $xs $ys
|
|
= case xs of
|
|
Nil => ys
|
|
Cons $x $zs => Cons x (cappend zs ys)
|
|
|
|
cvec : {n : _} -> Vect n $a -> Nat
|
|
cvec {n = $n} $xs
|
|
= case xs of
|
|
Nil => n
|
|
Cons $x $xs => n
|
|
|
|
cvec2 : {n : _} -> Vect n $a -> Nat
|
|
cvec2 {n = n@(_)} $xs
|
|
= case xs of
|
|
Nil => n
|
|
Cons $x $xs => n
|
|
|