git.iko.soy/Idris-dev
on master help sign in
Small formatting fix
3047ae8David Raymond Christiansen
src/Idris/Reflection.hs+4−2
compare with master
unifiedsplit
@@ -936,5 +936,7 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
936 | (cn, cty) <- constrs
936 | (cn, cty) <- constrs
937 ]
937 ]
938 ]
938 ]
939+ where reflectConArg (RParameter n t) =
939− where reflectConArg (RParameter n t) = raw_apply (Var $ tacN "Parameter") [reflectName n, reflectRaw t]
940+ raw_apply (Var $ tacN "Parameter") [reflectName n, reflectRaw t]
941+ reflectConArg (RIndex n t) =
940− reflectConArg (RIndex n t) = raw_apply (Var $ tacN "Index") [reflectName n, reflectRaw t]
942+ raw_apply (Var $ tacN "Index") [reflectName n, reflectRaw t]