arolle

open HolKernel boolLib bossLib Parse;
open listTheory rich_listTheory arithmeticTheory;

val _ = new_theory "listrev";

val LENGTH' = REWRITE_RULE[ADD1] LENGTH

(* specification of a reverse function f:
   elements of original list and f list are mirrored, i.e.
   an element at index            i         in  ls

arolle

#  New formally verified proof of #safegcd iteration bound:
#  https://cr.yp.to/2023/hull-light-20230416.sage (script for full
#  run+extras: https://cr.yp.to/2023/hull-light-howto-20230416.sh)
#  Advantages over previous formally verified proofs:
#  (1) covers all input sizes;
#  (2) finishes verifying in 10 minutes;
#  (3) smaller TCB (HOL Light).
#  https://twitter.com/hashbreaker/status/1647709221662646274#m

# assuming Debian or Ubuntu:

arolle

(*
Hashtable.empty size hashfunction comparison : ('a, 'b) Hashtable.hashtable
size : int
hashfunction : ('a -> int)
comparison : ('a -> 'a -> ordering)
*)

fun println str = TextIO.print (str ^ "\n");

val toStr = Int.toString;

arolle

Notes in the Terminal like in Notational Velocity

The way that Notational Velocity allows to manage your notes is genious, but only available to macOS users. That software presents a list of your notes next to the editable preview of a the selected note and a powerful full-text search filters the list of notes. As all the notes are stored as plain text files they can easily synchronized. This article presents an alternative note managing tool that works for major operating systems, is free and open source.

The setup combines ranger and ones' favourite

arolle

(:~
 : unix time from dateTime
 : @param dateTime
 : @return unix timestamp of the supplied datetime
 :)
declare local:dateTime-to-timestamp(
    $dateTime as xs:dateTime
) as xs:integer {
    let $dayZero := xs:dateTime('1970-01-01T00:00:00-00:00')
    return

arolle

declare namespace functx = "http://www.functx.com";

(: copied from functx :)
declare function functx:replace-multi
  ( $arg as xs:string? ,
    $changeFrom as xs:string* ,
    $changeTo as xs:string* ) as xs:string? {

   if (count($changeFrom) > 0)
   then functx:replace-multi(

arolle

(: 
 : protects all regexp special characters
 : @author Marc van Grootel
 : @see http://www.mail-archive.com/basex-talk@mailman.uni-konstanz.de/msg04573.html
 :)
declare function route:re-escape($string as xs:string)
    as xs:string {
    let $regexp-chars :=  ('.','*','+','|','?','(',')','[',']','{','}','^')
    return
        (: Note that '\' and '$' in the fold caused invalid pattern errors therefore put them in separate replace :)

arolle

(:~
 : Array Module
 : 
 : Implements Arrays in XQuery, according to the proposed
 : w3c working draft
 : http://www.w3.org/TR/xpath-functions-31/
 :
 : These arrays have the signature
 :   function(item()*, function(*)) as item()*
 : The Mogensen–Scott encoding is used to implement the data

arolle

" First step to make VIM an XQuery IDE using BaseX
" 
" Adds possibility to run the currently edited XQuery file
" using key combination <leader>r 
" An error output jumps to the file, line and column
" where the error occured.
" 


" associate *.bxs with xml filetype

arolle

(:
 : Snippet that makes the XML from the variable $xml available
 : to Javascript.
 :)
let $xml := <p>my text</p>
    ! serialize(.,
        <output:serialization-parameters>
          <output:method value="xml"/>
          <output:item-separator value=""/>
        </output:serialization-parameters>