Nick Drozd
Nick Drozd
This PR adds in some proofs from https://github.com/idris-lang/Idris-dev/pull/4841 without the major interface changes (there are some minor changes having to do with module organization). One big frustrating problem is that...
# Steps to Reproduce ```idris mtimes' : Monoid a => (n : Nat) -> a -> a mtimes' Z x = neutral mtimes' (S k) x = x mtimes' k...
Here's an ugly pattern, commonly found in eg config files: ```python config = {} config['dir'] = 'bin' config['user'] = 'me' config['workers'] = 5 ``` An empty dict is initialized and...
# Steps to Reproduce Stick this code at the bottom of Prelude.idr: ```idris interface Semigroup a => VerifiedSemigroup a where semigroupOpIsAssociative : (l, c, r : a) -> l (c...
The following pattern occurs a few times in the codebase: ```python while 1: data = conn.recv(blocksize) if not data: break ... ``` There is an unbounded `while` loop in which...
If I do a flickr keyword search, the default is to pull five random images (right?). But five images will be pulled even when there are fewer than five results...
If I use keyword `cat` and not output specified, I end up with files like `25112293657.jpg` and `30268200050.jpg`. It would be nice if these were called `cat-1.jpg`, `cat-2.jpg`, etc.
When no output is specified, the images are spewed into `.`. It would be nicer if the images were grouped into a directory instead, maybe call it `input-name-output`.
The other imports are builtins, so file mode can be used without installing anything.
I have a function `yield_programs`, and it calls a helper function `yield_actions`. Obviously they are a bit complicated; they were written like this for fun. They live together in the...