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

javascript - Laravel datatable invalid JSON response -

-
everything work fine on code below fetch user logs: js: <script> $(document).ready(function () { var table =$('#systemlogs').datatable({ responsive: true, processing: true, serverside: true, "language": { "url": "/datatables/media/plug-in/persian.json" }, ajax: '{!! url('/admin/systemlogs/data/systemlogsdatatable') !!}', columns: [ { data: 'name', name: 'name' }, { data: 'message_text', name: 'message_text' }, { data: 'remote_addr', name: 'remote_addr' }, { data: 'log_created_at', name: 'management_logs.created_at' }, { data: 'log_updated_at', name: 'management_logs.updated_at' }, ] }); }); </script> routes: route::get('/systemlogs/data/systemlogsdatatable','systemlogscontrolle...
Read more

java - Exception in thread "main" org.springframework.context.ApplicationContextException: Unable to start embedded container; -

-
i getting error when run spring application: exception in thread "main" org.springframework.context.applicationcontextexception: unable start embedded container; nested exception org.springframework.context.applicationcontextexception: unable start embeddedwebapplicationcontext due missing embeddedservletcontainerfactory bean. @ org.springframework.boot.context.embedded.embeddedwebapplicationcontext.onrefresh(embeddedwebapplicationcontext.java:124) @ org.springframework.context.support.abstractapplicationcontext.refresh(abstractapplicationcontext.java:476) @ org.springframework.boot.context.embedded.embeddedwebapplicationcontext.refresh(embeddedwebapplicationcontext.java:109) @ org.springframework.boot.springapplication.refresh(springapplication.java:691) @ org.springframework.boot.springapplication.run(springapplication.java:320) @ org.springframework.boot.springapplication.run(springapplication.java:952) @ org.springframework.boot.springa...
Read more

sql server 2008 - My Sql Code Get An Error Of Msg 245, Level 16, State 1, Line 1 Conversion failed when converting the varchar value '8:45 AM' to data type int -

-
msg 245, level 16, state 1, line 1 conversion failed when converting varchar value '8:45 am' data type int. script declare @specimenid bigint = 0, @script varchar(max); declare @starttime int = (select convert(int,substring(start_time,0,charindex(':', start_time)) - 12) appt appt._id=112601) --select @starttime set @script = 'select distinct ptlast_name + '', '' + pt.first_name patient_name, dbo.formatdate(pt.dob,''mm/dd/yyyy'') dob, (convert(varchar, (datediff(yy, dob, appt_date) - case when (month(dob) > month(appt_date)) or (month(dob) = month(appt_date) , day(dob) > day(appt_date)) 1 else 0 end)) + ''/'' + convert(varchar, (datediff(m, dateadd(yy, (datediff(yy, dob, appt_date) - case when (month(dob) > month(appt_date)) or (month(dob) = month(appt_date) , day(dob) > day(appt_date)) 1 else 0 end), d...
Read more