search

creichert / magit-gh-issues

Github issues extension for Magit
5 stars 2 forks source link

Test Issue #1

Open creichert opened 9 years ago

creichert commented 9 years ago

This Issue is open to test the functionality of this emacs extension

infixr 5 ::

data Vect : Nat -> Type -> Type where
    Nil  : Vect Z a
    (::) : a -> Vect k a -> Vect (S k) a

“Some half dozen persons have written technically on combinatory logic, and most of these, including ourselves, have published something erroneous. Since some of our fellow sinners are among the most careful and competent logicians on the contemporary scene, we regard this as evidence that the subject is refractory. Thus fullness of exposition is necessary for accuracy; and excessive condensation would be false economy here, even more than it is ordinarily.”

Haskell B. Curry and Robert Feys in the Preface to Combinatory Logic [3], May 31, 1956

creichert commented 9 years ago

Follow up comment with a suggestion.

app : Vect n a -> Vect m a -> Vect (n + m) a
app Nil       ys = ys
app (x :: xs) ys = x :: app xs ys