Idris2Doc : Core.Normalise.Convert

Core.Normalise.Convert

(source)
Reexports
import public Core.Normalise.Eval
import public Core.Normalise.Quote
Definitions
interface Convert : (List Name -> Type) -> Type
  Parameters: tm
Methods:
  
convert : Ref Ctxt Defs => Defs -> Env Term vars -> tm vars -> tm vars -> Core Bool
  
convertInf : Ref Ctxt Defs => Defs -> Env Term vars -> tm vars -> tm vars -> Core Bool
  
convGen : Ref Ctxt Defs => Ref QVar Int -> Bool -> Defs -> Env Term vars -> tm vars -> tm vars -> Core Bool

Implementations:
  
Convert NF
  
Convert Term
  
Convert Closure
convert : Convert tm => Ref Ctxt Defs => Defs -> Env Term vars -> tm vars -> tm vars -> Core Bool
  Visibility: public export
convertInf : Convert tm => Ref Ctxt Defs => Defs -> Env Term vars -> tm vars -> tm vars -> Core Bool
  Visibility: public export
convGen : Convert tm => Ref Ctxt Defs => Ref QVar Int -> Bool -> Defs -> Env Term vars -> tm vars -> tm vars -> Core Bool
  Visibility: public export