You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
%macrogetTTImp: v -> Elab TTImp
getTTImp v = quote v
u1 = getFC $ getTTImp ('a'=='b') -- this has physicalIdrSrc
u2 = getFC $ getTTImp (True==False) -- this has emptyFc
Motivation for this issue: Trying to implement some testing utilities
getFilePosition: TTImp -> String
getFilePosition x =case getFC x ofMkFC (PhysicalIdrSrc (MkMI path)) (line, column) _=>"\{foldl (\a, i => a "/" i) "src" $ reverse path}.idr:\{show $ line 1}:\{show column}"MkFC___=>"MkFC"MkVirtualFC___=>"MkVirtualFC"EmptyFC=>"EmptyFc"-- _ => ""public export
%macroassert: (()->Bool) -> Elab (IO())
assert condition =do
condition_quoted <- quote condition
let position = getFilePosition condition_quoted
let position_quoted =IPrimValEmptyFC (Str position)
check `(if~(condition_quoted) thenputStrLn"SUCCESS \{~(position_quoted)}"elseputStrLn"FAILURE \{~(position_quoted)}")
The text was updated successfully, but these errors were encountered:
Steps to Reproduce
Motivation for this issue: Trying to implement some testing utilities
The text was updated successfully, but these errors were encountered: