mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 02:07:25 +03:00
Fix typo
This commit is contained in:
parent
0119c217c9
commit
2d15b59e6d
@ -113,7 +113,7 @@ data Def : Type where
|
||||
(constraints : List Int) -> Def
|
||||
ImpBind : Def -- global name temporarily standing for an implicitly bound name
|
||||
-- A delayed elaboration. The elaborators themselves are stored in the
|
||||
-- unifiation state
|
||||
-- unification state
|
||||
Delayed : Def
|
||||
|
||||
export
|
||||
|
Loading…
Reference in New Issue
Block a user