Dependent typing, refinement types using SMT solver
Testing
Categorize words to specific domain
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; |
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 | } |
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 |
[<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 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 |
{-# 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 |
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>> } |
type CompareResult<'a, 'b> = | |
| FoundPair of 'a * 'b | |
| UnmatchedLHS of 'a | |
| UnmatchedRHS of 'b | |
[<RequireQualifiedAccess>] | |
module ListCompare = | |
let compare xsKeySelector ysKeySelector xs ys = | |
let xs = | |
xs |
open System;; | |
let random = new Random(); | |
let _rollTheDice (): (int|string) = | |
let number = random.Next(1, 6) | |
if (number >= 2) then number else "Winner" | |
let cls () = System.Console.Clear();; | |
type A = (int|string|int64) |