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

Require all definitions to be total in tests/typedd-book/chapter11/ArithCmdDo.idr

Browse Source
This commit is contained in:
Kamil Shakirov 2020-10-21 13:54:24 +06:00 committed by G. Allais
parent 71a638ef28
commit 127db79a6b
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/typedd-book/chapter11/ArithCmdDo.idr
View File

@ -2,7 +2,7 @@ import Data.Primitives.Views
import Data.Strings
import System
-- %default total
%default total
export
data Command : Type -> Type where