idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-29 03:24:02 +03:00
Code Issues Projects Releases Wiki Activity

Remove whitespace again

Browse Source 
Didn't I just do this? Grr.
This commit is contained in:
Edwin Brady 2021-05-26 15:54:57 +01:00
parent 9cce0e1340
commit a9b754e9fa
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tests/idris2/perf007/Slooow.idr
View File

@ -16,7 +16,7 @@ data TTy : Nat -> Nat -> Nat -> Nat -> Bool -> Type where
n : Nat -> Nat
n = (+ 2)
showInd : (indent : Nat) -> TTy p1 r1 v3 r3 br -> String
showInd i (TA x1 x2 x3) = if False
then (if False then show' i else show' i)