Clarification about Chris Done's question:
Let me split into two questions:
(1) What's the deal with "making the invariant inductive",
(2) If indeed the issue was (1) then why does this other fix* work?
Ranjit Jhala ranjitjhala
ranjitjhala
/ AVLTree.hs
Created
December 8, 2014 20:04
— forked from michaelbeaumont/AVLTree.hs
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module AVL where | |
| {-@ data Tree [ht] = Nil | Tree (x::Int) (l::Tree) (r::Tree) @-} | |
| data Tree = Nil | Tree Int Tree Tree | |
| {-@ height :: t:Tree -> {v:Int | v = ht t} @-} | |
| height :: Tree -> Int | |
| height Nil = 0 | |
| height (Tree _ l r) = (if height l > height r then 1 + height l else 1 + height r) |
ranjitjhala
/ gist:171aa922204aa84c7b3d
Last active
August 29, 2015 14:13
— forked from mpickering/gist:f1718fcdc4c56273ed52
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE ViewPatterns #-} | |
| module InTex where | |
| import Text.Pandoc.JSON | |
| import Text.Pandoc | |
| import Data.List | |
| main :: IO () | |
| main = toJSONFilter readFootnotes |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // Run at: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1427132944.hs | |
| module FizzBuzz where | |
| --------------------------------------------------------------- | |
| -- | Implementation: Top level | |
| --------------------------------------------------------------- | |
| main :: IO () | |
| main = mapM_ (putStrLn . say) (take 100 $ nums 0) |
ranjitjhala
/ shrink-lncs.sh
Last active
September 10, 2015 14:15
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/bin/bash | |
| pdfcrop --margins "5 10 5 20" --clip $1 crop.pdf | |
| pdfnup --nup 2x1 crop.pdf | |
| mv crop-nup.pdf $1 | |
| rm crop.pdf |
ranjitjhala
/ atom-typescript error
Created
September 18, 2015 02:24
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 0 info it worked if it ends with ok | |
| 1 verbose cli [ '/Applications/Atom.app/Contents/Resources/app/apm/bin/node', | |
| 1 verbose cli '/Applications/Atom.app/Contents/Resources/app/apm/node_modules/npm/bin/npm-cli.js', | |
| 1 verbose cli '--globalconfig', | |
| 1 verbose cli '/Users/rjhala/.atom/.apm/.apmrc', | |
| 1 verbose cli '--userconfig', | |
| 1 verbose cli '/Users/rjhala/.atom/.apmrc', | |
| 1 verbose cli 'rebuild', | |
| 1 verbose cli '--target=0.30.6', | |
| 1 verbose cli '--arch=x64' ] |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-@ LIQUID "--no-termination" @-} | |
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--no-adt" @-} | |
| {- LIQUID "--diff" @-} | |
| {-@ LIQUID "--ple" @-} | |
| module FingerTree where | |
| import Language.Haskell.Liquid.ProofCombinators |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (assert | |
| (and (and (= (= (- (- 3 1) 1) 7) false) | |
| (= (= (- 3 1) 4) false) | |
| (= | |
| (ite | |
| (= (- (- (- 3 1) 1) 1) 3) | |
| (foo (- (- (- (- 3 1) 1) 1) 1)) | |
| (ite | |
| (= (- (- (- 3 1) 1) 1) 2) | |
| (foo (- (- (- (- 3 1) 1) 1) 1)) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [client] run command: "/Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 --lsp" | |
| [client] debug command: "/Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 --lsp" | |
| [client] server cwd: undefined | |
| haskell-language-server version: 0.5.1.0 (GHC: 8.10.2) (PATH: /Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2) (GIT hash: e3fe0e7546aa91e44cc56cfe8ec078a026cf533a) | |
| Starting (haskell-language-server)LSP server... | |
| with arguments: LspArguments {argLSP = True, argsCwd = Nothing, argFiles = [], argsShakeProfiling = Nothing, argsTesting = False, argsExamplePlugin = False, argsDebugOn = False, argsLogFile = Nothing, argsThreads = 0, argsProjectGhcVersion = False} | |
| with plugins: [PluginId "brittany",PluginId "eval",PluginId "floskell",PluginId "fourmolu",PluginId "ghcide",PluginId "importLens",Plugi |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [client] run command: "/Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 --lsp" | |
| [client] debug command: "/Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 --lsp" | |
| [client] server cwd: undefined | |
| haskell-language-server version: 0.5.1.0 (GHC: 8.10.2) (PATH: /Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2) (GIT hash: e3fe0e7546aa91e44cc56cfe8ec078a026cf533a) | |
| Starting (haskell-language-server)LSP server... | |
| with arguments: LspArguments {argLSP = True, argsCwd = Nothing, argFiles = [], argsShakeProfiling = Nothing, argsTesting = False, argsExamplePlugin = False, argsDebugOn = False, argsLogFile = Nothing, argsThreads = 0, argsProjectGhcVersion = False} | |
| with plugins: [PluginId "brittany",PluginId "eval",PluginId "floskell",PluginId "fourmolu",PluginId "ghcide",PluginId "importLens",Plugi |
OlderNewer