MarcelineVQ

pilot Nash Smash
date 13 12 3015
system Alhena
planet Mainsail
clearance
travel "Epsilon Leonis"
travel Gomeisa
travel Dubhe
travel Tejat
"reputation with"

MarcelineVQ

<lcvette_> ok
<lcvette_> so scratch the idea of moving crap around
<lcvette_> ill get the 8300 elite
<lcvette_> although i hate buying used stuff
<lcvette_> im the guy who is the 1 in xx who you hear about
<pcw_home> Of the 15 or so motherboards I have none except the slowest atoms (330,D525) have such bad latency with Preempt-RT at 1 KHz
<pcw_home> you could also run the servo thread slower for the time being
<lcvette_> i feel like i want the h97 and g3258, because they are new
<lcvette_> and you said good
<lcvette_> its a drop in the bucket at this point

MarcelineVQ

total
revInvolutiveHelp : (xs : List a) -> (ys : List a) ->
                    reverse' xs ++ ys = reverse' (reverse' ys ++ xs)
revInvolutiveHelp xs [] =
       rewrite appendNilRightNeutral (reverse' xs)
    in Refl
revInvolutiveHelp xs (x :: ys) =
       rewrite sym (appendAssociative (reverse' ys) [x] xs)
    in rewrite sym (revInvolutiveHelp (x :: xs) ys)
    in rewrite sym (appendAssociative (reverse' xs) [x] ys)

MarcelineVQ

combine_odd_even' : (podd, peven : Nat -> Type) -> (Nat -> Type)
combine_odd_even' podd peven n with (evenb n)
combine_odd_even' podd peven n | False = podd n
combine_odd_even' podd peven n | True = peven n

combine_odd_even_intro : (n : Nat) ->
(oddb n = True -> podd n) ->
(oddb n = False -> peven n) ->
combine_odd_even' podd peven n
combine_odd_even_intro k f g with (evenb k)

MarcelineVQ

combine_odd_even' : (podd, peven : Nat -> Type) -> (Nat -> Type)
combine_odd_even' podd peven n with (evenb n)
  combine_odd_even' podd peven n | False = podd n
  combine_odd_even' podd peven n | True = peven n

combine_odd_even_intro : (n : Nat) ->
                         (oddb n = True -> podd n) ->
                         (oddb n = False -> peven n) ->
                         combine_odd_even' podd peven n
combine_odd_even_intro k f g with (evenb k)

MarcelineVQ

<Aaryan> Hello !
<srhb> o/
<Aaryan> I am an undergradute freshman, and am highly interested about the project idea listed under here https://summer.haskell.org/ideas.html#algebraic-graphs
<Aaryan> And I would like some help on how to get started
<srhb> Aaryan: This query is probably very relevant in #haskell as well. What I would do is immediately contact some of the people who have been mentors on this topic previously, as well as find knowledgable people by going through the committers on github.
<srhb> Aaryan: Direct contact, and quickly, is key to sorting out what to do here.
* crissava has quit (Quit: Konversation terminated!)
* Big_G (~Big_G@50-46-196-19.evrt.wa.frontiernet.net) has joined
* merijn has quit (Ping timeout: 250 seconds)
* Ox37b has quit (Ping timeout: 244 seconds)

MarcelineVQ

%default total

data Two : Type where
  TT : Two
  FF : Two

So : Two -> Type
So TT = ()
So FF = Void

MarcelineVQ

-- This works

Eitha : Type -> Type -> Type
Eitha b a = Either a b

[eitha]
Functor (Eitha b) where
  map f (Left l) = Left (f l)
  map f (Right r) = Right r

MarcelineVQ

namespace MyVect
  my_map : (a -> b) -> Vect n a -> Vect n b


namespace MyVect {

my_map : (a -> b) -> Vect n a -> Vect n b

}

MarcelineVQ

--loop, I don't even use pffft
guess : (target : Nat) -> IO ()
guess target = do
  printLn "Rate die Zahl"
  line <- getLine
  Just g <- pure (stringToNat line) | Nothing => (printLn "Invalid String" *> guess target)
  let pffft = stringToNat line
  let g = case stringToNat line of
            Just p => p
            Nothing => 0