expression.txt

(define isTwo
  (fun ([:a Int] [-> Bool])
    (if (eq? x 2)
      True
      False)))

(define add
  (fun ([:a Int] [-> Int])
   (do 
    


 
    end)))


(define month
  (fun ([:a Int] [-> Int])
    (case n    --注意这里是有有一个常量的值的
      ((1) 31)
      ((2) 28)
      ((9) 50))))
 
 (typename [a :class (U Ord Num)])
 (define abs
  (fun ([:a T] [:b T] [-> a.type])
    (cond       --但是在这里是没有常量的值的
      ((n > 0) n)
      (else (- n 1)))))

----------poly------------
(define $
  (fun (f x)
    (f x)))

($ f x)

(define add
  (fun (f b)
   (f b)))

-----------------这里进行证明
(add (assert (:f (Int –> Int)) 
             (:a Int)) 
             addInt 2)

----------------------------
(define gold
  (fun (x)
    (assert (goldbach-conjecture x))
    x))

(define bar
  (fun (z)
    (gold (assume (goldbach-conjecture x))
          (gold z))))

(define bar
  (fun (z)
    (print z)
    (Resut A)))

----是否在函数参数列表中加入模式匹配
def add(:addone, a) do
	a + 1
end

add(:addone, 1)

#这样的不可以, 因为不匹配
add(:addTwo, 2) 

add函数有两个参数第一个参数是
:addone 是一个值
a是一个变量

### 感觉这种不太好
### 1. 参数既可以绑定到变量上
### 2. 参数也可以是与值或符号进行匹配


def print_multiple_times(msg, n) do
   if n == 0 do
      :ok
   else
     print n
     print_multiple_times(msg, n - 1)
  end
end