是否可以在Idris的成語括號中使用條件語句？

Question

像下面的表達式是非常有效的在伊德里斯：

let x = Just 5 in let y = Just 6 in [|x/y|] 

有人能寫出像下面的表達式？

let x = Just 5 in let y = Just 6 in [| if x == 0 then 0 else y|] 

我似乎無法得到它編譯。

Answer 1

我能採取的兩個問題護理得到這個工作：

1. if _ then _ else _似乎並不成語支架傳播到其子表達式

2. 的if _ then _ else _默認定義是（當然）在它的兩個分支懶惰，並且Lazy' LazyEval似乎不解除實例。

一旦解決了這兩個問題，我就可以在成語括號中找到它。但請注意，這對於採用兩個分支都具有可觀察效果的應用程序不起作用。

strictIf : Bool -> a -> a -> a 
strictIf True t e = t 
strictIf False t e = e 

syntax "if" [b] "then" [t] "else" [e] = strictIf b t e 

test : Maybe Float 
test = let x = Just 5 
      y = Just 6 
     in [| if [| x == pure 0 |] then [|0|] else y |]