Reference in Coq Lists library not found -

-

i'm trying use concat function appears in https://coq.inria.fr/distrib/current/stdlib/coq.lists.list.html. tried following:

require import arith coq.lists.list. import listnotations.  definition con (l : list nat):= (concat [[0]; l]).

but error error: reference concat not found in current environment. thought should work since i've imported library, don't know error comes from.

i'm using version 8.4pl3 (january 2014). version issue?

concat added in this commit. think close end of 8.4pl3 release not pushed release, rather next 8.5


Comments

Post a Comment

Popular posts from this blog

wireshark - USB mapping with python -

-
while reading ctf write-ups came across script #!/usr/bin/env python import struct import image import dpkt init_x, init_y = 100, 400 def print_map(pcap, device): picture = image.new("rgb", (1200, 500), "white") pixels = picture.load() x, y = init_x, init_y ts, buf in pcap: device_id, = struct.unpack("b", buf[0x0b]) if device_id != device: continue data = struct.unpack("bbbb", buf[-4:]) status = data[0] x = x + data[1] y = y + data[2] if (status == 1): in range(-5, 5): j in range(-5, 5): pixels[x + , y + j] = (0, 0, 0, 0) else: pixels[x, y] = (255, 0, 0, 0) picture.save("riverside-map.png", "png") if __name__ == "__main__": f = open("usb.pcap", "rb") pcap = dpkt.pcap.reader(f) print_map(pcap, 5) f.close() and ...
Read more

c++ - nodejs socket.io closes connection before upgrading to websocket -

-
i'm trying write c++ client talk websocket server written using nodejs , socket.io. can't c++ client establish websocket connection; server drops connection right after client requests http connection upgraded websocket. i used tcpdump watch packets going , forth. when use websocket server browser, works great , tcpdump output shows packets going , forth. when try connect server using c++ client, websocket connection never gets established. output tcpdump shows upgrade request being sent server followed server dropping connection. i tried replicating sequence of events using nc . connected server (running on port 8080) , copy-pasted exact set of headers sent browser, captured tcpdump. duplicate of working headers, connection dropped. there no output on server end indicating why connection gets dropped. here headers sent: get /socket.io/?type=player&eio=3&transport=websocket&sid=7mdclht_8ctsd6f4aaac http/1.1 host: localhost:8080 connection: upgrade prag...
Read more

Deploying Qt Application on Android is really slow? -

-
as may know there 3 ways deploy qt application on android : use ministro service install qt deploy local qt libraries temporary directory bundle qt libraries in apk the first method takes 30 seconds , needs install apk . ministro . second takes 1 minute me ! , anytime try run program qt creator pushes qt libraries device. third 1 makes .apk file big , again takes 1 minute me. think situation that's not reasonable develop android application using qt. there way make deploying process faster? almost full year since op , things have not changed @ all. deployment of 7 mb apk takes on minute , half project compiles in 5 seconds. reason answering not problem got resolved, offer alternative solution. i've implemented "workaround" consisting of 2 applications work in tandem - 1 on pc , 1 on device - created compile files remotely, turned out faster alternative deployment well. on host create application launches compilation in separate process, when do...
Read more