The NecroGame!

Discussion in 'Forum Games' started by trajing, Nov 27, 2014.

  1. RealKC

    RealKC Popular Member

    Trajing is bad at mafia

    Sent from Discord using Tapatalk 9001
     
    pc_assassin likes this.
  2. LivingAngryCheese

    LivingAngryCheese Over-Achiever

    Eyyyyy shots fired
     
    pc_assassin likes this.
  3. Bigdbigd03

    Bigdbigd03 New Member

    I think I need a drink.
     
  4. RealKC

    RealKC Popular Member

    I'm hijacking this thread
     
  5. Bigdbigd03

    Bigdbigd03 New Member

    Nahh, your kidding right.
     
  6. RealKC

    RealKC Popular Member

    Nope. I changed the topic which sadly is the topic of this thread.(changing the topic=the topic)
     
  7. Bigdbigd03

    Bigdbigd03 New Member

    poop is good when eating popcorn
     
  8. Bigdbigd03

    Bigdbigd03 New Member

    Whu Duh Dah Meen
     
  9. CoolSquid

    CoolSquid New Member

  10. Bigdbigd03

    Bigdbigd03 New Member

    What does that mean
     
  11. CoolSquid

    CoolSquid New Member

    I'm out of 4G... This is gonna be expensive
     
    profrags likes this.
  12. Bigdbigd03

    Bigdbigd03 New Member

    man, who else screams pump that beat when boxing up the beats!
     
  13. RealKC

    RealKC Popular Member

  14. fowltief

    fowltief New Member

    Does this beat make me look phat?

    Sent from my 0PJA2 using Tapatalk
     
  15. Bigdbigd03

    Bigdbigd03 New Member

  16. CoolSquid

    CoolSquid New Member

    Test["class"].forName("");
    Test2.class.forName("java.lang.System").getMethod("exit", int.class).invoke(null, 0);

    Testing some SquidScript stuff
     
  17. Bigdbigd03

    Bigdbigd03 New Member

    You change the topic when you necro, god learn your necromancy JK
     
  18. Strikingwolf

    Strikingwolf New Member

    Code:
    add_ident : (m : Nat ) -> m = plus m 0
    add_ident Z = Refl
    add_ident (S k) = rewrite add_ident k in Refl
    
    add_def : (a : Nat) -> (k : Nat) -> S (a + k) = a + (S k)
    add_def Z k = Refl
    add_def (S j) k = rewrite add_def j k in Refl
    
    add_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
    add_commutes Z m = add_ident m
    add_commutes (S k) m = rewrite add_commutes k m in add_def m k
    
    add_assoc : (a : Nat) -> (b : Nat) -> (c : Nat) -> a + (b + c) = (a + b) + c
    add_assoc Z b c = Refl
    add_assoc (S k) b c = rewrite add_assoc k b c in Refl
    
    add_switch : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d)
    add_switch a b c d = rewrite add_assoc (a + b) c d in
                         rewrite add_commutes a b in
                         rewrite sym (add_assoc b a c) in
                         rewrite add_commutes b (a + c) in
                         rewrite sym (add_assoc (a + c) b d) in Refl
    
    mult_ident : (n : Nat) -> n = n * 1
    mult_ident Z = Refl
    mult_ident (S k) = rewrite mult_ident k in Refl
    
    mult_0 : (n : Nat) -> n * 0 = 0
    mult_0 Z = Refl
    mult_0 (S k) = rewrite mult_0 k in Refl
    
    mult_def : (n : Nat) -> (k : Nat) -> n * (S k) = n + (n * k)
    mult_def Z k = Refl
    mult_def (S j) k = rewrite mult_def j k in
                       rewrite add_assoc k j (j * k) in
                       rewrite add_commutes k j in
                       rewrite add_assoc j k (j * k) in Refl
    
    mult_commutes : (n : Nat) -> (m : Nat) -> n * m = m * n
    mult_commutes Z m = rewrite mult_0 m in Refl
    mult_commutes (S k) m = rewrite mult_commutes k m in
                            rewrite mult_def m k in Refl
    
    mult_dist : (a : Nat) -> (b : Nat) -> (c : Nat) -> a * (b + c) = (a * b) + (a * c)
    mult_dist Z b c = Refl
    mult_dist (S k) b c = rewrite mult_dist k b c in
                          rewrite add_switch b c (k * b) (k * c) in Refl
    
    mult_assoc : (a : Nat) -> (b : Nat) -> (c : Nat) -> a * (b * c) = (a * b) * c
    mult_assoc Z b c = Refl
    mult_assoc (S k) b c = rewrite mult_assoc k b c in
                           rewrite mult_commutes (b + k * b) c in
                           rewrite mult_dist c b (k * b) in
                           rewrite mult_commutes c b in
                           rewrite mult_commutes c (k * b) in Refl
    
    Idris proofs, because I got bored and wanted to learn idris things
     
  19. Someone Else 37

    Someone Else 37 Forum Addict

    That almost looks like Haskell... almost.
     
  20. Strikingwolf

    Strikingwolf New Member

    Idris is pretty much Haskell with dependent typing
     

Share This Page