mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 02:07:25 +03:00
commit
2542c325b1
@ -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