docker run --name synquid -it yinengy/synquid
synquid <your_program_filename>

/var/www/comcom/tmp/Synquid/9586857029030353/Synquid.sq:29: Error:
Cannot match shape 'List (A4)'
with shape 'Int'
when checking...

-- Type synonym for natural numbers (_v denotes the "value variable")
type Nat = {Int | _v >= 0}

-- List data type: just like in Haskell
data List a where
	Nil :: List a
	Cons :: x: a -> xs: List a -> List a
  
-- Measures define recursive properties of datatypes, which we can mention in refinements; 
-- this measure is also marked as a termination metric for recursive calls
termination measure len :: List a -> {Int | _v >= 0} where
  Nil -> 0
  Cons x xs -> 1 + len xs 
  
-- Synquid composes programs from component functions;
-- here are some standard integer components we might need
one :: {Int | _v == 1}
minus :: x: Int -> {Int | _v == (0 - x)}
plus :: x: Int -> y: Int -> {Int | _v == x + y}
leq :: x: Int -> y: Int -> {Bool | _v == (x <= y)}
	
-- Our synthesis goal: a function that returns 'n' copies of 'x'
replicate :: n: Nat -> x: a -> {List a | len _v == n}
replicate = ??

replicate :: n: Nat -> x: a -> {List a | len _v == n}

replicate :: x: a -> {List a | len _v == 4}

/var/www/comcom/tmp/Synquid/0719913783814785/Synquid.sq:29: Error:
Cannot match shape 'Bool'
with shape '_'
when checking neq :: X1:_ -> X0:_ -> _
in
\x .
match neq ?? ?? with

replicate :: x: a -> {List a | len _v == 3}

replicate = \x . Cons x (Cons x (Cons x Nil))