mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
Correct a couple of minor typos in the effects package idrisdoc
This commit is contained in:
parent
095fb31160
commit
c67d49cf05
@ -73,8 +73,8 @@ data FileHandle : (m : Mode) -> Type where
|
||||
-- ---------------------------------------------- [ Resource Type Construction ]
|
||||
|
||||
||| Calculates the type for the resource being computed over. `Unit`
|
||||
||| to describe pre-and-post file handle acquisistion, and `FileHandle
|
||||
||| m` when a file handle has been aqcuired.
|
||||
||| to describe pre-and-post file handle acquisition, and `FileHandle
|
||||
||| m` when a file handle has been acquired.
|
||||
|||
|
||||
||| @m The mode the file handle was generated under.
|
||||
||| @ty The functions return type.
|
||||
@ -315,7 +315,7 @@ R = FileHandle Read
|
||||
W : Type
|
||||
W = FileHandle WriteTruncate
|
||||
|
||||
||| A file can only be appeneded to.
|
||||
||| A file can only be appended to.
|
||||
A : Type
|
||||
A = FileHandle Append
|
||||
|
||||
@ -324,7 +324,7 @@ RW : Type
|
||||
RW = FileHandle ReadWrite
|
||||
|
||||
||| A file opened for reading and writing and has been truncated to
|
||||
||| zero if it previsiouly existed.
|
||||
||| zero if it previously existed.
|
||||
RWPlus : Type
|
||||
RWPlus = FileHandle ReadWriteTruncate
|
||||
|
||||
|
@ -130,7 +130,7 @@ initLogger l cs = call $ InitLogger l cs
|
||||
|||
|
||||
||| @l The logging level.
|
||||
||| @cs The logging categories.
|
||||
||| @m THe message to be logged.
|
||||
||| @m The message to be logged.
|
||||
log : (Show a, Eq a) => (l : LogLevel n)
|
||||
-> (cs : List a)
|
||||
-> (m : String)
|
||||
@ -141,7 +141,7 @@ log l cs msg = call $ Log l cs msg
|
||||
|||
|
||||
||| @l The logging level.
|
||||
||| @cs The logging categories.
|
||||
||| @m THe message to be logged.
|
||||
||| @m The message to be logged.
|
||||
logN : (Show a, Eq a) => (l : Nat)
|
||||
-> {auto prf : LTE l 70}
|
||||
-> (cs : List a)
|
||||
|
@ -193,7 +193,7 @@ collectPMetrics b = call $ TurnOn b
|
||||
collectPMetricsAndShow : Eff () [PERF]
|
||||
collectPMetricsAndShow = call $ TurnOn True
|
||||
|
||||
||| Return gatheres metrics
|
||||
||| Return gathered metrics
|
||||
getPerfMetrics : Eff PMetrics [PERF]
|
||||
getPerfMetrics = call $ GetMetrics
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user