Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Mar 23 2015 05:27
    domdere commented #3
  • Mar 23 2015 05:26

    domdere on master

    Update to current Idris version… Merge pull request #3 from Heat… (compare)

  • Mar 23 2015 05:26
    domdere closed #3
  • Mar 22 2015 19:35
    Heather opened #3
  • Mar 08 2015 12:42
    ekmett commented #1
  • Mar 08 2015 12:42
    ekmett closed #1
  • Mar 08 2015 10:44
    domdere commented #1
  • Mar 08 2015 10:25
    ekmett reopened #1
  • Mar 08 2015 10:25
    ekmett closed #1
  • Mar 08 2015 07:43
    domdere commented #2
  • Mar 08 2015 07:43

    domdere on master

    resolve issue #1 ;) Merge pull request #2 from Heat… (compare)

  • Mar 08 2015 07:43
    domdere closed #2
  • Mar 08 2015 05:42
    Heather opened #2
  • Mar 08 2015 05:03
    ekmett opened #1
Dom De Re
@domdere
blah
Mark Bradley
@barkmadley
neat
Dom De Re
@domdere
yeah you can type code in too
foldr :: (a -> b) -> b -> [a] -> b
and get it marked up
dont think there is syntax highlighting for idris yet though :/
Pascal Voitot
@mandubian
Hey people, stupid question about a non-compiling case I don't understand
data Member : Type -> Vect n Type -> Type where
  Found : Member x (x :: xs)
  Next  : Member x xs -> Member x (y :: xs)

data Cop : Vect n Type -> Type where
  In : x -> {auto prf: Member x xs} -> Cop xs

-- OK
i: Int
i = 5
s: Cop [String, Int]
s = In i

-- OK (as expected)
s2: Cop [String, Int]
s2 = In 5 { prf = Next Found }

-- KO with "String is not a numeric type"
s1: Cop [String, Int]
s1 = In 5
any idea where I failed?
Patrik Andersson
@pandemonium

I'm new to Idris and I'm struggling with how to satisfy a sized Vect-type with a list. This:

suitSize : Nat
suitSize = 13

frequencies : Hand -> Vect suitSize Nat
frequencies hand =
[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13]

fails with a type missmatch specifically between 13 and suitSize. I've tried various combinations using the `the´ combinator but to no avail. If I replace suitSize with 13 this compiles. What am I missing here?

Patrik Andersson
@pandemonium
Okay - so it seems I'm being bitten by shadowing/ aliasing. The suitSize I give as part of the type of the return value of frequencies is not from the function by that name.
Dom De Re
@domdere
@pandemonium so it worked when you used ModuleName.suitSize in the type right?
Patrik Andersson
@pandemonium
I didn't try that - I went with a type alias instead.
But that does work! Thank you :)
Patrik Andersson
@pandemonium
So, can a record have a field of type Fin n that can be updated with the record syntax? I get compiler errors about a missing set_<field-name> where :t field-name is Fin n
It feels like a really stupid question :)
Writing a Brainfuck interpreter because reasons and I would really like to restrict the pointer field of the interpreter state to the length of the memory Vect
Patrik Andersson
@pandemonium
I understand now. So of course I cannot change one of two fields that are joined by one having a type dependent on the other
Răzvan Flavius Panda
@razvan-panda
Anyone would be interested in joining a group about artificial general intelligence / strong AI? https://gitter.im/artificial-general-intelligence/Lobby
doofin
@doofin
Hi guys, I have some question about c ffi, How to bind to abstract types when using ffi ?
data TF_Status
tfNewStatus : IO TF_Status tfNewStatus = foreign FFI_C "TF_NewStatus" (IO TF_Status)
it complains that When checking argument fty to function foreign: Can't find a value of type FTy FFI_C [] (IO TF_Status)