Dependent typing, refinement types using SMT solver
Testing
Categorize words to specific domain
type private InternalElement<'Key, 'Value when 'Key: comparison> = | |
{ key: 'Key | |
data: 'Value | |
polygon: Polygon } | |
[<Struct>] | |
type STRtree<'Key, 'Value when 'Key: comparison> = | |
private { map: Map<'Key, InternalElement<'Key, 'Value>> | |
strTree: NetTopologySuite.Index.Strtree.STRtree<InternalElement<'Key, 'Value>> } |
Dependent typing, refinement types using SMT solver
Testing
Categorize words to specific domain
{-# LANGUAGE NumDecimals #-} | |
swapNodes :: Int -> [a] -> [a] | |
swapNodes _ [] = [] | |
swapNodes k z = swapNodes' z [] | |
where | |
swapNodes' [] acc = acc | |
swapNodes' x acc = | |
let (a,b) = splitAt k x | |
firstHalf = if (length a < k) then |
module Snl.Api.V1.Types where | |
import Data.Aeson | |
import Data.Proxy | |
import Data.Swagger | |
import Data.Time | |
import Data.UUID as UUID | |
import GHC.Generics | |
import Servant.API | |
import Snl.Core.Types |
[<AutoOpen>] | |
module Quantex.Common.Prelude | |
type Range<'T> = { From: 'T; To: 'T } | |
module Range = | |
let create (r: 'T * 'T) = | |
let (a,b) = r | |
if (a >= b) then Error("From cannot be greater than To") else Ok({ From = a; To = b}) | |
type Range<'T> with |
module App.View | |
open Elmish | |
open Fable.React | |
open Fable.React.Props | |
open State | |
open Types | |
open Fulma | |
open Fable.FontAwesome | |
open Fable.FontAwesome.Free |
Executing task: cargo build < | |
Compiling shell v0.1.0 (file:///home/swoorup/github/mysh-rs) | |
error[E0597]: `input` does not live long enough | |
--> src/main.rs:30:25 | |
| | |
30 | lexer.tokenize(&input); | |
| ^^^^^ borrowed value does not live long enough | |
... | |
38 | } |
import std.array; | |
import std.stdio; | |
import std.exception; | |
import std.string; | |
import std.conv : to; | |
import std.algorithm.searching; | |
import std.algorithm.iteration; | |
import erupted; | |
import derelict.sdl2.sdl; |
-*- mode: compilation; default-directory: "~/Dropbox/vulkan_experiments/vkapp/" -*- | |
Compilation started at Sat Dec 31 15:28:03 | |
time dub | |
Performing "debug" build using dmd for x86_64. | |
derelict-util 2.0.6: target for configuration "library" is up to date. | |
derelict-sdl2 2.0.2: target for configuration "library" is up to date. | |
xcb-d 2.1.0+1.11.1: target for configuration "library" is up to date. | |
xlib-d 0.1.1: target for configuration "library" is up to date. | |
vulkantriangled ~master: building configuration "application"... |
;; This file was obtained from | |
;; http://forum.dlang.org/post/[email protected] | |
(defun run-current-project-args (args) | |
(setq cmdStr (concat "time dub " args)) | |
(setq buffname (format "*%s*" cmdStr)) | |
(save-excursion | |
(message (concat "Running:" cmdStr)) | |
(if (not (eq nil (get-buffer buffname))) (kill-buffer buffname)) | |
(setq compilation-scroll-output t) |