Commit 15eda3f5 authored by andy@galois.com's avatar andy@galois.com
Browse files

an expression with a TickBox round it is not in HNF.

parent ec3c7841
......@@ -620,6 +620,10 @@ exprIsHNF (Lit l) = True
exprIsHNF (Type ty) = True -- Types are honorary Values;
-- we don't mind copying them
exprIsHNF (Lam b e) = isRuntimeVar b || exprIsHNF e
exprIsHNF (Note (TickBox {}) _)
= False
exprIsHNF (Note (BinaryTickBox {}) _)
= False
exprIsHNF (Note _ e) = exprIsHNF e
exprIsHNF (Cast e co) = exprIsHNF e
exprIsHNF (App e (Type _)) = exprIsHNF e
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment