atondwal

LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.


**** DONE:  A-Normalization ****************************************************
 

**** DONE:  Extracted Core using GHC *******************************************
 

**** DONE:  Transformed Core ***************************************************

atondwal

Lists
=====


<div class="hidden">
\begin{code}
{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--no-termination" @-}

{-# LANGUAGE DeriveGeneric #-}

atondwal

stack exec -- liquid --savequery tests/pos/AVLRJ.hs
stack exec -- liquid --savequery tests/pos/Ackermann.hs
stack exec -- liquid --savequery tests/pos/AmortizedQueue.hs
stack exec -- liquid --savequery tests/pos/Avg.hs
stack exec -- liquid --savequery tests/pos/Constraints.hs
stack exec -- liquid --savequery tests/pos/DB00.hs
stack exec -- liquid --savequery tests/pos/Even.hs
stack exec -- liquid --savequery tests/pos/GCD.hs
stack exec -- liquid --savequery tests/pos/Graph.hs
stack exec -- liquid --savequery tests/pos/LambdaEvalSuperTiny.hs

atondwal

stack exec -- fixpoint -i ../tests/pos/.liquid/AVLRJ.hs.fq &&
echo AVLRJ.hs.fq >> tests.succ
stack exec -- fixpoint -i ../tests/pos/.liquid/Ackermann.hs.fq &&
echo Ackermann.hs.fq >> tests.succ
stack exec -- fixpoint -i ../tests/pos/.liquid/AmortizedQueue.hs.fq &&
echo AmortizedQueue.hs.fq >> tests.succ
stack exec -- fixpoint -i ../tests/pos/.liquid/Avg.hs.fq &&
echo Avg.hs.fq >> tests.succ
stack exec -- fixpoint -i ../tests/pos/.liquid/Constraints.hs.fq &&
echo Constraints.hs.fq >> tests.succ

atondwal

.
├── 2cellos
│   └── 2cellos
│       ├── 2cellos-Misirlou.m4a
│       ├── 2cellos-Smells_Like_Teen_Spirit.m4a
│       ├── 2cellos-Smooth_Criminal.m4a
│       ├── 2cellos-The_Resistance.m4a
│       ├── 2cellos-Use_Somebody.m4a
│       └── 2cellos-Viva_La_Vida.m4a
├── 3_Doors_Down

atondwal

AnishTondwalkarBelloHUM ILack of moderation in Frankenstein Alphonse Frankenstein urges Victor to express moderation, and in some ways serves as foil to Victor Frankenstein. His moderation in emotion keeps him away from large problems until his son drags him into them. He lives an ordinary life for his place in the socioeconomic ladder, and he is generally happy. Whenever he is not happy, it is directly or indirectly due to Victor Frankenstein, who easily moved by his his emotions, and will act on tiny impulses, much unlike Alphonse himself.

atondwal

Anish Tondwalkar Bello HUM I

The Role of Religion in Comforting People in Cry, The Beloved Country

“Who indeed knows the secret of the earthly pilgrimage? Who knows for what we live, and struggle, and die?” (62).\

atondwal

Verifying that +ani_sh is my blockchain ID. https://onename.com/ani_sh

atondwal

Keybase proof

I hereby claim:

• I am atondwal on github.
• I am tondwalkar (https://keybase.io/tondwalkar) on keybase.
• I have a public key ASDxmfMhnDtyNMmO_qKCRmC5MBwNrRRloThBe3-Yf3aE-wo

To claim this, I am signing this object:

atondwal

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)
(set-option :smt.mbqi false)
(define-sort Elt () Int)
(define-sort Set () (Array Elt Bool))
(define-fun smt_set_emp () Set ((as const Set) false))
(define-fun smt_set_mem ((x Elt) (s Set)) Bool (select s x))
(define-fun smt_set_add ((s Set) (x Elt)) Set (store s x true))
(define-fun smt_set_cup ((s1 Set) (s2 Set)) Set ((_ map or) s1 s2))