Skip to content

Instantly share code, notes, and snippets.

@timjs

timjs/HelloWorld.icl

Created January 20, 2017 21:27
Show Gist options
  • Save timjs/863dd2295fb5bb0e3203e75c3e8688aa to your computer and use it in GitHub Desktop.
Save timjs/863dd2295fb5bb0e3203e75c3e8688aa to your computer and use it in GitHub Desktop.
Download ZIP
Compiled version of HelloWorld.idr to Clean
Raw
HelloWorld.icl
module HelloWorld
import StdEnv
import StdPointer
:: Value = Nothing
| Boxed_Bool !Bool
| Boxed_Char !Char
| Boxed_Int !Int
| Boxed_Real !Real
| Boxed_String !String
| ..
unbox_Bool (Boxed_Bool x) :== x
unbox_Char (Boxed_Char x) :== x
unbox_Int (Boxed_Int x) :== x
unbox_Real (Boxed_Real x) :== x
unbox_String (Boxed_String x) :== x
clean_String_cons (Boxed_Char chr) (Boxed_String str) :== Boxed_String (toString chr +++ str)
clean_String_reverse (Boxed_String str) :== Boxed_String { str.[i] \\ i <- reverse [0..size str - 1] }
clean_String_head (Boxed_String str) :== Boxed_Char (select str 0)
clean_String_tail (Boxed_String str) :== Boxed_String (str % (1, size str - 1))
clean_String_index (Boxed_String str) (Boxed_Int i) :== Boxed_Char (select str i)
clean_String_len (Boxed_String str) :== Boxed_Int (size str)
clean_String_substring (Boxed_Int ofs) (Boxed_Int len) (Boxed_String str) :== Boxed_String (str % (ofs, ofs + len - 1))
clean_System_write_String world (Boxed_String str) | clean_Prim_toStdout str :== Nothing
clean_System_read_String world
# (str, ok) = clean_Prim_fromStdin
| ok :== Boxed_String str
clean_System_numArgs world :== Boxed_Int (fst clean_Prim_args)
clean_System_getArgs (Boxed_Int idx) :== Boxed_String ((snd clean_Prim_args) !! idx)
clean_Prim_toStdout :: !String -> Bool
clean_Prim_toStdout str = code inline {
.d 1 0
jsr stdioF
.o 1 2 f
.d 1 2 f
jsr writeFS
.o 0 2 f
.d 0 2 f
jsr closeF
.o 0 1 b
}
clean_Prim_fromStdin :: (!String,!Bool)
clean_Prim_fromStdin = code inline {
.d 0 0
jsr stdioF
.o 0 2 f
.d 0 2 f
jsr readLineF
.o 1 2 f
.d 0 2 f
jsr closeF
.o 0 1 b
}
clean_Prim_args :: (!Int, [String])
clean_Prim_args
# argc = readInt32Z global_argc 0
# argv = derefInt global_argv
= (argc, [derefString (readInt argv (i << (IF_INT_64_OR_32 3 2)) ) \\ i <- [0..argc - 1]])
:: Value /// ForeignEnv.:: (1)
| Idris_ForeignEnv__58__58_
/// Prelude.List.:: (1)
| Idris_Prelude_List__58__58_ !Value !Value
/// Prelude.Stream.:: (0)
| Idris_Prelude_Stream__58__58_ !Value
/// = (65536)
| Idris__61_ !Value !Value !Value !Value
/// Language.Reflection.ATDouble (1)
| Idris_Language_Reflection_ATDouble
/// Language.Reflection.ATInt (0)
| Idris_Language_Reflection_ATInt
/// Language.Reflection.AType (9)
| Idris_Language_Reflection_AType
/// Prelude.WellFounded.Access (0)
| Idris_Prelude_WellFounded_Access
/// Prelude.WellFounded.Accessible (65537)
| Idris_Prelude_WellFounded_Accessible !Value !Value !Value
/// Prelude.Nat.Additive (65538)
| Idris_Prelude_Nat_Additive
/// Language.Reflection.AllTypes (2)
| Idris_Language_Reflection_AllTypes
/// Language.Reflection.Errors.AlreadyDefined (28)
| Idris_Language_Reflection_Errors_AlreadyDefined
/// Prelude.Applicative.Alternative (65539)
| Idris_Prelude_Applicative_Alternative !Value
/// Language.Reflection.App (3)
| Idris_Language_Reflection_App
/// Prelude.Show.App (6)
| Idris_Prelude_Show_App
/// Prelude.File.Append (2)
| Idris_Prelude_File_Append
/// Prelude.Applicative.Applicative (65540)
| Idris_Prelude_Applicative_Applicative !Value
/// Language.Reflection.ApplyTactic (12)
| Idris_Language_Reflection_ApplyTactic
/// Language.Reflection.ArithTy (65541)
| Idris_Language_Reflection_ArithTy
/// Language.Reflection.B16 (6)
| Idris_Language_Reflection_B16
/// Language.Reflection.B32 (7)
| Idris_Language_Reflection_B32
/// Language.Reflection.B64 (8)
| Idris_Language_Reflection_B64
/// Language.Reflection.B8 (5)
| Idris_Language_Reflection_B8
/// Language.Reflection.BI (1)
| Idris_Language_Reflection_BI
/// Prelude.Show.Backtick (3)
| Idris_Prelude_Show_Backtick
/// Language.Reflection.Bind (2)
| Idris_Language_Reflection_Bind
/// Language.Reflection.Binder (65542)
| Idris_Language_Reflection_Binder !Value
/// Prelude.Bool.Bool (65543)
| Idris_Prelude_Bool_Bool
/// Ownership.Borrowed (65544)
| Idris_Ownership_Borrowed !Value
/// Language.Reflection.Bound (0)
| Idris_Language_Reflection_Bound
/// Language.Reflection.ByReflection (14)
| Idris_Language_Reflection_ByReflection
/// CData (65545)
| Idris_CData
/// FFI_C.CFnPtr (65546)
| Idris_FFI_C_CFnPtr !Value
/// FFI_C.C_Any (5)
| Idris_FFI_C_C_Any
/// FFI_C.C_CData (8)
| Idris_FFI_C_C_CData
/// FFI_C.C_Float (1)
| Idris_FFI_C_C_Float
/// FFI_C.C_Fn (0)
| Idris_FFI_C_C_Fn
/// FFI_C.C_FnBase (2)
| Idris_FFI_C_C_FnBase
/// FFI_C.C_FnIO (1)
| Idris_FFI_C_C_FnIO
/// FFI_C.C_FnT (6)
| Idris_FFI_C_C_FnT
/// FFI_C.C_FnTypes (65547)
| Idris_FFI_C_C_FnTypes !Value
/// FFI_C.C_IntBits16 (3)
| Idris_FFI_C_C_IntBits16
/// FFI_C.C_IntBits32 (4)
| Idris_FFI_C_C_IntBits32
/// FFI_C.C_IntBits64 (5)
| Idris_FFI_C_C_IntBits64
/// FFI_C.C_IntBits8 (2)
| Idris_FFI_C_C_IntBits8
/// FFI_C.C_IntChar (0)
| Idris_FFI_C_C_IntChar
/// FFI_C.C_IntNative (1)
| Idris_FFI_C_C_IntNative
/// FFI_C.C_IntT (7)
| Idris_FFI_C_C_IntT
/// FFI_C.C_IntTypes (65548)
| Idris_FFI_C_C_IntTypes !Value
/// FFI_C.C_MPtr (3)
| Idris_FFI_C_C_MPtr
/// FFI_C.C_Ptr (2)
| Idris_FFI_C_C_Ptr
/// FFI_C.C_Str (0)
| Idris_FFI_C_C_Str
/// FFI_C.C_Types (65549)
| Idris_FFI_C_C_Types !Value
/// FFI_C.C_Unit (4)
| Idris_FFI_C_C_Unit
/// Language.Reflection.Errors.CantConvert (4)
| Idris_Language_Reflection_Errors_CantConvert
/// Language.Reflection.Errors.CantInferType (7)
| Idris_Language_Reflection_Errors_CantInferType
/// Language.Reflection.Errors.CantIntroduce (11)
| Idris_Language_Reflection_Errors_CantIntroduce
/// Language.Reflection.Errors.CantMatch (14)
| Idris_Language_Reflection_Errors_CantMatch
/// Language.Reflection.Errors.CantResolve (17)
| Idris_Language_Reflection_Errors_CantResolve
/// Language.Reflection.Errors.CantResolveAlts (19)
| Idris_Language_Reflection_Errors_CantResolveAlts
/// Language.Reflection.Errors.CantSolveGoal (5)
| Idris_Language_Reflection_Errors_CantSolveGoal
/// Language.Reflection.Errors.CantUnify (2)
| Idris_Language_Reflection_Errors_CantUnify
/// Language.Reflection.Case (20)
| Idris_Language_Reflection_Case
/// Language.Reflection.CaseN (5)
| Idris_Language_Reflection_CaseN
/// Prelude.Cast.Cast (65550)
| Idris_Prelude_Cast_Cast !Value !Value
/// Language.Reflection.Ch (3)
| Idris_Language_Reflection_Ch
/// Language.Reflection.Claim (4)
| Idris_Language_Reflection_Claim
/// Prelude.Nat.CmpEQ (1)
| Idris_Prelude_Nat_CmpEQ
/// Prelude.Nat.CmpGT (2)
| Idris_Prelude_Nat_CmpGT
/// Prelude.Nat.CmpLT (0)
| Idris_Prelude_Nat_CmpLT
/// Prelude.Nat.CmpNat (65551)
| Idris_Prelude_Nat_CmpNat !Value !Value
/// Language.Reflection.Compute (23)
| Idris_Language_Reflection_Compute
/// Language.Reflection.Const (65552)
| Idris_Language_Reflection_Const
/// Language.Reflection.Elab.Constraint (2)
| Idris_Language_Reflection_Elab_Constraint
/// Language.Reflection.Elab.Constructor (0)
| Idris_Language_Reflection_Elab_Constructor
/// Language.Reflection.Elab.ConstructorDefn (65553)
| Idris_Language_Reflection_Elab_ConstructorDefn
/// Language.Reflection.Elab.CtorArg (65554)
| Idris_Language_Reflection_Elab_CtorArg
/// Language.Reflection.Elab.CtorField (1)
| Idris_Language_Reflection_Elab_CtorField
/// Language.Reflection.Elab.CtorParameter (0)
| Idris_Language_Reflection_Elab_CtorParameter
/// Language.Reflection.DCon (2)
| Idris_Language_Reflection_DCon
/// FFI_Export.DHere (0)
| Idris_FFI_Export_DHere
/// Builtins.DPair (65555)
| Idris_Builtins_DPair !Value !Value
/// FFI_Export.DThere (1)
| Idris_FFI_Export_DThere
/// FFI_Export.Data (0)
| Idris_FFI_Export_Data !Value !Value !Value
/// FFI_Export.DataDefined (65556)
| Idris_FFI_Export_DataDefined !Value !Value !Value !Value
/// Language.Reflection.Elab.DataDefn (65557)
| Idris_Language_Reflection_Elab_DataDefn
/// Language.Reflection.Elab.Datatype (65558)
| Idris_Language_Reflection_Elab_Datatype
/// Prelude.Basics.Dec (65559)
| Idris_Prelude_Basics_Dec !Value
/// Decidable.Equality.DecEq (65560)
| Idris_Decidable_Equality_DecEq !Value
/// Language.Reflection.Elab.Declare (0)
| Idris_Language_Reflection_Elab_Declare
/// Language.Reflection.Elab.DefineDatatype (0)
| Idris_Language_Reflection_Elab_DefineDatatype
/// Language.Reflection.Elab.DefineFun (0)
| Idris_Language_Reflection_Elab_DefineFun
/// Delay (0)
| Idris_Delay
/// DelayReason (65561)
| Idris_DelayReason
/// Delayed (65562)
| Idris_Delayed !Value !Value
/// Prelude.Show.Dollar (2)
| Idris_Prelude_Show_Dollar
/// Prelude.Interfaces.EQ (1)
| Idris_Prelude_Interfaces_EQ
/// Prelude.Either.Either (65563)
| Idris_Prelude_Either_Either !Value !Value
/// Language.Reflection.Elab.Elab (65564)
| Idris_Language_Reflection_Elab_Elab !Value
/// Prelude.Pairs.Element (0)
| Idris_Prelude_Pairs_Element
/// Language.Reflection.ElimN (6)
| Idris_Language_Reflection_ElimN
/// FFI_Export.End (2)
| Idris_FFI_Export_End
/// Prelude.Enum (65565)
| Idris_Prelude_Enum !Value
/// Prelude.Interfaces.Eq (65566)
| Idris_Prelude_Interfaces_Eq !Value
/// Prelude.Show.Eq (1)
| Idris_Prelude_Show_Eq
/// Language.Reflection.Elab.Erased (0)
| Idris_Language_Reflection_Elab_Erased
/// Language.Reflection.Erased (5)
| Idris_Language_Reflection_Erased
/// Language.Reflection.Elab.Erasure (65567)
| Idris_Language_Reflection_Elab_Erasure
/// Language.Reflection.Errors.Err (65568)
| Idris_Language_Reflection_Errors_Err
/// Prelude.Providers.Error (1)
| Idris_Prelude_Providers_Error
/// Language.Reflection.ErrorReportPart (65569)
| Idris_Language_Reflection_ErrorReportPart
/// Prelude.Pairs.Evidence (0)
| Idris_Prelude_Pairs_Evidence
/// Language.Reflection.Exact (16)
| Idris_Language_Reflection_Exact
/// Prelude.Pairs.Exists (65570)
| Idris_Prelude_Pairs_Exists !Value !Value
/// Language.Reflection.Elab.Explicit (0)
| Idris_Language_Reflection_Elab_Explicit
/// ForeignEnv.FEnv (65571)
| Idris_ForeignEnv_FEnv !Value !Value
/// FFI (65572)
| Idris_FFI
/// FFI_Export.FFI_Base (65573)
| Idris_FFI_Export_FFI_Base !Value !Value !Value
/// FFI_Export.FFI_ExpType (0)
| Idris_FFI_Export_FFI_ExpType !Value !Value
/// FFI_Export.FFI_Export (65574)
| Idris_FFI_Export_FFI_Export !Value !Value !Value
/// FFI_Export.FFI_Exportable (65575)
| Idris_FFI_Export_FFI_Exportable !Value !Value !Value
/// FFI_Export.FFI_Fun (1)
| Idris_FFI_Export_FFI_Fun !Value !Value
/// FFI_Export.FFI_IO (0)
| Idris_FFI_Export_FFI_IO !Value
/// FFI_Export.FFI_Prim (1)
| Idris_FFI_Export_FFI_Prim !Value
/// FFI_Export.FFI_Ret (2)
| Idris_FFI_Export_FFI_Ret !Value
/// FFun (1)
| Idris_FFun
/// Prelude.File.FHandle (0)
| Idris_Prelude_File_FHandle !Value
/// FRet (0)
| Idris_FRet
/// FTy (65576)
| Idris_FTy !Value !Value !Value
/// Language.Reflection.Fail (25)
| Idris_Language_Reflection_Fail
/// Prelude.Bool.False (0)
| Idris_Prelude_Bool_False
/// Prelude.File.File (65577)
| Idris_Prelude_File_File
/// Prelude.File.FileError (65578)
| Idris_Prelude_File_FileError
/// Language.Reflection.FileLoc (0)
| Idris_Language_Reflection_FileLoc
/// Prelude.File.FileNotFound (3)
| Idris_Prelude_File_FileNotFound
/// Prelude.File.FileReadError (1)
| Idris_Prelude_File_FileReadError
/// Prelude.File.FileWriteError (2)
| Idris_Prelude_File_FileWriteError
/// Language.Reflection.Fill (15)
| Idris_Language_Reflection_Fill
/// Language.Reflection.Elab.Fixity (65579)
| Idris_Language_Reflection_Elab_Fixity
/// Language.Reflection.Fl (2)
| Idris_Language_Reflection_Fl
/// Language.Reflection.Focus (17)
| Idris_Language_Reflection_Focus
/// Prelude.Foldable.Foldable (65580)
| Idris_Prelude_Foldable_Foldable !Value
/// Language.Reflection.Forgot (12)
| Idris_Language_Reflection_Forgot
/// Prelude.Interfaces.Fractional (65581)
| Idris_Prelude_Interfaces_Fractional !Value
/// FFI_Export.Fun (1)
| Idris_FFI_Export_Fun !Value !Value !Value !Value
/// Language.Reflection.Elab.FunArg (65582)
| Idris_Language_Reflection_Elab_FunArg
/// Language.Reflection.Elab.FunClause (65583)
| Idris_Language_Reflection_Elab_FunClause !Value
/// Language.Reflection.Elab.FunDefn (65584)
| Idris_Language_Reflection_Elab_FunDefn !Value
/// Prelude.Functor.Functor (65585)
| Idris_Prelude_Functor_Functor !Value
/// Language.Reflection.GHole (4)
| Idris_Language_Reflection_GHole
/// Prelude.Interfaces.GT (2)
| Idris_Prelude_Interfaces_GT
/// Prelude.File.GenericFileError (0)
| Idris_Prelude_File_GenericFileError
/// Prelude.Nat.GetAdditive (0)
| Idris_Prelude_Nat_GetAdditive
/// Prelude.Nat.GetMultiplicative (0)
| Idris_Prelude_Nat_GetMultiplicative
/// Language.Reflection.GoalType (1)
| Idris_Language_Reflection_GoalType
/// Language.Reflection.Guess (5)
| Idris_Language_Reflection_Guess
/// Language.Reflection.Hole (3)
| Idris_Language_Reflection_Hole
/// Language.Reflection.I (0)
| Idris_Language_Reflection_I
/// IO' (65586)
| Idris_IO_39_ !Value !Value
/// Language.Reflection.IT16 (1)
| Idris_Language_Reflection_IT16
/// Language.Reflection.IT32 (2)
| Idris_Language_Reflection_IT32
/// Language.Reflection.IT64 (3)
| Idris_Language_Reflection_IT64
/// Language.Reflection.IT8 (0)
| Idris_Language_Reflection_IT8
/// Language.Reflection.ITBig (2)
| Idris_Language_Reflection_ITBig
/// Language.Reflection.ITChar (3)
| Idris_Language_Reflection_ITChar
/// Language.Reflection.ITFixed (0)
| Idris_Language_Reflection_ITFixed
/// Language.Reflection.ITNative (1)
| Idris_Language_Reflection_ITNative
/// Language.Reflection.Implementation (8)
| Idris_Language_Reflection_Implementation
/// Language.Reflection.ImplementationCtorN (7)
| Idris_Language_Reflection_ImplementationCtorN
/// Language.Reflection.ImplementationN (2)
| Idris_Language_Reflection_ImplementationN
/// Language.Reflection.Elab.Implicit (1)
| Idris_Language_Reflection_Elab_Implicit
/// Prelude.List.InBounds (65587)
| Idris_Prelude_List_InBounds !Value !Value !Value
/// Prelude.List.InFirst (0)
| Idris_Prelude_List_InFirst
/// Prelude.List.InLater (1)
| Idris_Prelude_List_InLater
/// Language.Reflection.Errors.Inaccessible (25)
| Idris_Language_Reflection_Errors_Inaccessible
/// Language.Reflection.Errors.IncompleteTerm (21)
| Idris_Language_Reflection_Errors_IncompleteTerm
/// Language.Reflection.Induction (19)
| Idris_Language_Reflection_Induction
/// Infinite (0)
| Idris_Infinite
/// Language.Reflection.Errors.InfiniteUnify (3)
| Idris_Language_Reflection_Errors_InfiniteUnify
/// Language.Reflection.Elab.Infix (2)
| Idris_Language_Reflection_Elab_Infix
/// Language.Reflection.Elab.Infixl (0)
| Idris_Language_Reflection_Elab_Infixl
/// Language.Reflection.Elab.Infixr (1)
| Idris_Language_Reflection_Elab_Infixr
/// Language.Reflection.IntTy (65588)
| Idris_Language_Reflection_IntTy
/// Prelude.Interfaces.Integral (65589)
| Idris_Prelude_Interfaces_Integral !Value
/// Language.Reflection.Errors.InternalMsg (1)
| Idris_Language_Reflection_Errors_InternalMsg
/// Language.Reflection.Intro (11)
| Idris_Language_Reflection_Intro
/// Language.Reflection.Intros (10)
| Idris_Language_Reflection_Intros
/// Language.Reflection.Errors.InvalidTCArg (18)
| Idris_Language_Reflection_Errors_InvalidTCArg
/// Prelude.Maybe.IsJust (65590)
| Idris_Prelude_Maybe_IsJust !Value !Value
/// Prelude.List.IsNonEmpty (0)
| Idris_Prelude_List_IsNonEmpty
/// Prelude.Maybe.ItIsJust (0)
| Idris_Prelude_Maybe_ItIsJust
/// JS_Float (1)
| Idris_JS_Float
/// JS_Fn (0)
| Idris_JS_Fn
/// JS_FnBase (2)
| Idris_JS_FnBase
/// JS_FnIO (1)
| Idris_JS_FnIO
/// JS_FnT (4)
| Idris_JS_FnT
/// JS_FnTypes (65591)
| Idris_JS_FnTypes !Value
/// JS_IntChar (0)
| Idris_JS_IntChar
/// JS_IntNative (1)
| Idris_JS_IntNative
/// JS_IntT (5)
| Idris_JS_IntT
/// JS_IntTypes (65592)
| Idris_JS_IntTypes !Value
/// JS_Ptr (2)
| Idris_JS_Ptr
/// JS_Str (0)
| Idris_JS_Str
/// JS_Types (65593)
| Idris_JS_Types !Value
/// JS_Unit (3)
| Idris_JS_Unit
/// JsFn (65594)
| Idris_JsFn !Value
/// Prelude.Maybe.Just (1)
| Idris_Prelude_Maybe_Just !Value
/// Prelude.Interfaces.LT (0)
| Idris_Prelude_Interfaces_LT
/// Prelude.Nat.LTE (65595)
| Idris_Prelude_Nat_LTE !Value !Value
/// Prelude.Nat.LTESucc (1)
| Idris_Prelude_Nat_LTESucc
/// Prelude.Nat.LTEZero (0)
| Idris_Prelude_Nat_LTEZero
/// Language.Reflection.Lam (0)
| Idris_Language_Reflection_Lam
/// LazyValue (1)
| Idris_LazyValue
/// Prelude.Either.Left (0)
| Idris_Prelude_Either_Left !Value
/// Prelude.Nat.LeftIsNotZero (0)
| Idris_Prelude_Nat_LeftIsNotZero
/// Language.Reflection.Let (2)
| Idris_Language_Reflection_Let
/// Language.Reflection.LetTac (21)
| Idris_Language_Reflection_LetTac
/// Language.Reflection.LetTacTy (22)
| Idris_Language_Reflection_LetTacTy
/// Prelude.List.List (65596)
| Idris_Prelude_List_List !Value
/// Language.Reflection.Errors.LoadingFailed (32)
| Idris_Language_Reflection_Errors_LoadingFailed
/// Language.Reflection.MN (2)
| Idris_Language_Reflection_MN
/// ManagedPtr (65597)
| Idris_ManagedPtr
/// Prelude.Interfaces.MaxBound (65598)
| Idris_Prelude_Interfaces_MaxBound !Value
/// Prelude.Maybe.Maybe (65599)
| Idris_Prelude_Maybe_Maybe !Value
/// Language.Reflection.MetaN (8)
| Idris_Language_Reflection_MetaN
/// Language.Reflection.MethodN (4)
| Idris_Language_Reflection_MethodN
/// Prelude.Interfaces.MinBound (65600)
| Idris_Prelude_Interfaces_MinBound !Value
/// FFI_C.MkCFnPtr (0)
| Idris_FFI_C_MkCFnPtr !Value
/// Builtins.MkDPair (0)
| Idris_Builtins_MkDPair
/// Language.Reflection.Elab.MkDatatype (0)
| Idris_Language_Reflection_Elab_MkDatatype
/// MkFFI (0)
| Idris_MkFFI
/// Language.Reflection.Elab.MkFunArg (0)
| Idris_Language_Reflection_Elab_MkFunArg
/// Language.Reflection.Elab.MkFunClause (0)
| Idris_Language_Reflection_Elab_MkFunClause
/// MkIO (0)
| Idris_MkIO !Value
/// Language.Reflection.Elab.MkImpossibleClause (1)
| Idris_Language_Reflection_Elab_MkImpossibleClause
/// MkJsFn (0)
| Idris_MkJsFn !Value
/// Builtins.MkPair (0)
| Idris_Builtins_MkPair !Value !Value
/// FFI_C.MkRaw (0)
| Idris_FFI_C_MkRaw !Value
/// Builtins.MkUPair (0)
| Idris_Builtins_MkUPair !Value !Value
/// MkUnit (0)
| Idris_MkUnit
/// Prelude.File.Mode (65601)
| Idris_Prelude_File_Mode
/// Prelude.Monad.Monad (65602)
| Idris_Prelude_Monad_Monad !Value
/// Prelude.Algebra.Monoid (65603)
| Idris_Prelude_Algebra_Monoid !Value
/// Language.Reflection.Errors.Msg (0)
| Idris_Language_Reflection_Errors_Msg
/// Prelude.Nat.Multiplicative (65604)
| Idris_Prelude_Nat_Multiplicative
/// Language.Reflection.NS (1)
| Idris_Language_Reflection_NS
/// Language.Reflection.NamePart (1)
| Idris_Language_Reflection_NamePart
/// Language.Reflection.NameType (65605)
| Idris_Language_Reflection_NameType
/// Prelude.Nat.Nat (65606)
| Idris_Prelude_Nat_Nat
/// Language.Reflection.NativeTy (65607)
| Idris_Language_Reflection_NativeTy
/// Prelude.Interfaces.Neg (65608)
| Idris_Prelude_Interfaces_Neg !Value
/// ForeignEnv.Nil (0)
| Idris_ForeignEnv_Nil
/// Prelude.List.Nil (0)
| Idris_Prelude_List_Nil
/// Prelude.Basics.No (1)
| Idris_Prelude_Basics_No
/// Language.Reflection.Errors.NoEliminator (22)
| Idris_Language_Reflection_Errors_NoEliminator
/// Language.Reflection.Errors.NoRewriting (30)
| Idris_Language_Reflection_Errors_NoRewriting
/// Language.Reflection.Errors.NoSuchVariable (12)
| Idris_Language_Reflection_Errors_NoSuchVariable
/// Language.Reflection.Errors.NoTypeDecl (15)
| Idris_Language_Reflection_Errors_NoTypeDecl
/// Language.Reflection.Errors.NoValidAlts (20)
| Idris_Language_Reflection_Errors_NoValidAlts
/// Language.Reflection.Errors.NonCollapsiblePostulate (27)
| Idris_Language_Reflection_Errors_NonCollapsiblePostulate
/// Prelude.List.NonEmpty (65609)
| Idris_Prelude_List_NonEmpty !Value !Value
/// Language.Reflection.Errors.NonFunctionType (8)
| Idris_Language_Reflection_Errors_NonFunctionType
/// Prelude.Nat.NotBothZero (65610)
| Idris_Prelude_Nat_NotBothZero !Value !Value
/// Language.Reflection.Errors.NotEquality (9)
| Idris_Language_Reflection_Errors_NotEquality
/// Language.Reflection.Elab.NotErased (1)
| Idris_Language_Reflection_Elab_NotErased
/// Language.Reflection.Errors.NotInjective (16)
| Idris_Language_Reflection_Errors_NotInjective
/// Prelude.Maybe.Nothing (0)
| Idris_Prelude_Maybe_Nothing
/// Language.Reflection.NullType (0)
| Idris_Language_Reflection_NullType
/// Prelude.Interfaces.Num (65611)
| Idris_Prelude_Interfaces_Num !Value
/// Prelude.Show.Open (0)
| Idris_Prelude_Show_Open
/// Prelude.Interfaces.Ord (65612)
| Idris_Prelude_Interfaces_Ord !Value
/// Prelude.Interfaces.Ordering (65613)
| Idris_Prelude_Interfaces_Ordering
/// Language.Reflection.P (0)
| Idris_Language_Reflection_P
/// Language.Reflection.PVTy (7)
| Idris_Language_Reflection_PVTy
/// Language.Reflection.PVar (6)
| Idris_Language_Reflection_PVar
/// Builtins.Pair (65614)
| Idris_Builtins_Pair !Value !Value
/// Language.Reflection.ParentN (3)
| Idris_Language_Reflection_ParentN
/// Prelude.File.PermissionDenied (4)
| Idris_Prelude_File_PermissionDenied
/// Language.Reflection.Pi (1)
| Idris_Language_Reflection_Pi
/// Language.Reflection.Elab.Plicity (65615)
| Idris_Language_Reflection_Elab_Plicity
/// Prelude.Show.Prec (65616)
| Idris_Prelude_Show_Prec
/// Language.Reflection.Elab.Prefix (3)
| Idris_Language_Reflection_Elab_Prefix
/// Prelude.Show.PrefixMinus (5)
| Idris_Prelude_Show_PrefixMinus
/// PrimIO (65617)
| Idris_PrimIO !Value
/// Language.Reflection.Elab.Prim__AddImplementation (38)
| Idris_Language_Reflection_Elab_Prim__AddImplementation
/// Language.Reflection.Elab.Prim__Apply (18)
| Idris_Language_Reflection_Elab_Prim__Apply
/// Language.Reflection.Elab.Prim__Attack (22)
| Idris_Language_Reflection_Elab_Prim__Attack
/// Language.Reflection.Elab.Prim__BindElab (1)
| Idris_Language_Reflection_Elab_Prim__BindElab
/// Language.Reflection.Elab.Prim__Check (12)
| Idris_Language_Reflection_Elab_Prim__Check
/// Language.Reflection.Elab.Prim__Claim (24)
| Idris_Language_Reflection_Elab_Prim__Claim
/// Language.Reflection.Elab.Prim__Compute (30)
| Idris_Language_Reflection_Elab_Prim__Compute
/// Language.Reflection.Elab.Prim__Converts (33)
| Idris_Language_Reflection_Elab_Prim__Converts
/// Language.Reflection.Elab.Prim__Debug (44)
| Idris_Language_Reflection_Elab_Prim__Debug
/// Language.Reflection.Elab.Prim__DeclareDatatype (36)
| Idris_Language_Reflection_Elab_Prim__DeclareDatatype
/// Language.Reflection.Elab.Prim__DeclareType (34)
| Idris_Language_Reflection_Elab_Prim__DeclareType
/// Language.Reflection.Elab.Prim__DefineDatatype (37)
| Idris_Language_Reflection_Elab_Prim__DefineDatatype
/// Language.Reflection.Elab.Prim__DefineFunction (35)
| Idris_Language_Reflection_Elab_Prim__DefineFunction
/// Language.Reflection.Elab.Prim__Env (4)
| Idris_Language_Reflection_Elab_Prim__Env
/// Language.Reflection.Elab.Prim__Fail (3)
| Idris_Language_Reflection_Elab_Prim__Fail
/// Language.Reflection.Elab.Prim__Fill (17)
| Idris_Language_Reflection_Elab_Prim__Fill
/// Language.Reflection.Elab.Prim__Fixity (43)
| Idris_Language_Reflection_Elab_Prim__Fixity
/// Language.Reflection.Elab.Prim__Focus (20)
| Idris_Language_Reflection_Elab_Prim__Focus
/// Language.Reflection.Elab.Prim__Forall (26)
| Idris_Language_Reflection_Elab_Prim__Forall
/// Language.Reflection.Elab.Prim__Gensym (15)
| Idris_Language_Reflection_Elab_Prim__Gensym
/// Language.Reflection.Elab.Prim__Goal (5)
| Idris_Language_Reflection_Elab_Prim__Goal
/// Language.Reflection.Elab.Prim__Guess (7)
| Idris_Language_Reflection_Elab_Prim__Guess
/// Language.Reflection.Elab.Prim__Holes (6)
| Idris_Language_Reflection_Elab_Prim__Holes
/// Prim__IO (0)
| Idris_Prim__IO !Value
/// Language.Reflection.Elab.Prim__Intro (25)
| Idris_Language_Reflection_Elab_Prim__Intro
/// Language.Reflection.Elab.Prim__IsTCName (39)
| Idris_Language_Reflection_Elab_Prim__IsTCName
/// Language.Reflection.Elab.Prim__LetBind (29)
| Idris_Language_Reflection_Elab_Prim__LetBind
/// Language.Reflection.Elab.Prim__LookupArgs (11)
| Idris_Language_Reflection_Elab_Prim__LookupArgs
/// Language.Reflection.Elab.Prim__LookupDatatype (9)
| Idris_Language_Reflection_Elab_Prim__LookupDatatype
/// Language.Reflection.Elab.Prim__LookupFunDefn (10)
| Idris_Language_Reflection_Elab_Prim__LookupFunDefn
/// Language.Reflection.Elab.Prim__LookupTy (8)
| Idris_Language_Reflection_Elab_Prim__LookupTy
/// Language.Reflection.Elab.Prim__MatchApply (19)
| Idris_Language_Reflection_Elab_Prim__MatchApply
/// Language.Reflection.Elab.Prim__Metavar (45)
| Idris_Language_Reflection_Elab_Prim__Metavar
/// Language.Reflection.Elab.Prim__Namespace (14)
| Idris_Language_Reflection_Elab_Prim__Namespace
/// Language.Reflection.Elab.Prim__Normalise (31)
| Idris_Language_Reflection_Elab_Prim__Normalise
/// Language.Reflection.Elab.Prim__PatBind (28)
| Idris_Language_Reflection_Elab_Prim__PatBind
/// Language.Reflection.Elab.Prim__PatVar (27)
| Idris_Language_Reflection_Elab_Prim__PatVar
/// Language.Reflection.Elab.Prim__PureElab (0)
| Idris_Language_Reflection_Elab_Prim__PureElab
/// Language.Reflection.Elab.Prim__RecursiveElab (42)
| Idris_Language_Reflection_Elab_Prim__RecursiveElab
/// Language.Reflection.Elab.Prim__ResolveTC (40)
| Idris_Language_Reflection_Elab_Prim__ResolveTC
/// Language.Reflection.Elab.Prim__Rewrite (23)
| Idris_Language_Reflection_Elab_Prim__Rewrite
/// Language.Reflection.Elab.Prim__Search (41)
| Idris_Language_Reflection_Elab_Prim__Search
/// Language.Reflection.Elab.Prim__Solve (16)
| Idris_Language_Reflection_Elab_Prim__Solve
/// Language.Reflection.Elab.Prim__SourceLocation (13)
| Idris_Language_Reflection_Elab_Prim__SourceLocation
/// Language.Reflection.Elab.Prim__Try (2)
| Idris_Language_Reflection_Elab_Prim__Try
/// Language.Reflection.Elab.Prim__Unfocus (21)
| Idris_Language_Reflection_Elab_Prim__Unfocus
/// Language.Reflection.Elab.Prim__Whnf (32)
| Idris_Language_Reflection_Elab_Prim__Whnf
/// Language.Reflection.Errors.ProgramLineComment (24)
| Idris_Language_Reflection_Errors_ProgramLineComment
/// Language.Reflection.Errors.ProofSearchFail (29)
| Idris_Language_Reflection_Errors_ProofSearchFail
/// Prelude.Providers.Provide (0)
| Idris_Prelude_Providers_Provide
/// Prelude.Providers.Provider (65618)
| Idris_Prelude_Providers_Provider !Value
/// Language.Reflection.Errors.ProviderError (31)
| Idris_Language_Reflection_Errors_ProviderError
/// Ptr (65619)
| Idris_Ptr
/// Language.Reflection.Quotable (65620)
| Idris_Language_Reflection_Quotable !Value !Value
/// Language.Reflection.RApp (2)
| Idris_Language_Reflection_RApp
/// Language.Reflection.RBind (1)
| Idris_Language_Reflection_RBind
/// Language.Reflection.RConstant (5)
| Idris_Language_Reflection_RConstant
/// Language.Reflection.RType (3)
| Idris_Language_Reflection_RType
/// Language.Reflection.RUType (4)
| Idris_Language_Reflection_RUType
/// FFI_C.Raw (65621)
| Idris_FFI_C_Raw !Value
/// Language.Reflection.Raw (65622)
| Idris_Language_Reflection_Raw
/// Language.Reflection.RawPart (3)
| Idris_Language_Reflection_RawPart
/// Prelude.File.Read (0)
| Idris_Prelude_File_Read
/// Ownership.Read (0)
| Idris_Ownership_Read
/// Prelude.File.ReadAppend (5)
| Idris_Prelude_File_ReadAppend
/// Prelude.File.ReadWrite (3)
| Idris_Prelude_File_ReadWrite
/// Prelude.File.ReadWriteTruncate (4)
| Idris_Prelude_File_ReadWriteTruncate
/// Language.Reflection.Ref (1)
| Idris_Language_Reflection_Ref
/// Language.Reflection.Refine (2)
| Idris_Language_Reflection_Refine
/// Refl (0)
| Idris_Refl
/// Language.Reflection.ReflConst (65623)
| Idris_Language_Reflection_ReflConst !Value
/// Language.Reflection.Reflect (13)
| Idris_Language_Reflection_Reflect
/// Language.Reflection.Rewrite (18)
| Idris_Language_Reflection_Rewrite
/// Prelude.Either.Right (1)
| Idris_Prelude_Either_Right !Value
/// Prelude.Nat.RightIsNotZero (1)
| Idris_Prelude_Nat_RightIsNotZero
/// Prelude.Nat.S (1)
| Idris_Prelude_Nat_S
/// Language.Reflection.SN (3)
| Idris_Language_Reflection_SN
/// Language.Reflection.Search (7)
| Idris_Language_Reflection_Search
/// Prelude.Algebra.Semigroup (65624)
| Idris_Prelude_Algebra_Semigroup !Value
/// Language.Reflection.Seq (3)
| Idris_Language_Reflection_Seq
/// Prelude.Show.Show (65625)
| Idris_Prelude_Show_Show !Value
/// Language.Reflection.Skip (24)
| Idris_Language_Reflection_Skip
/// Language.Reflection.Solve (9)
| Idris_Language_Reflection_Solve
/// Language.Reflection.SourceFC (26)
| Idris_Language_Reflection_SourceFC
/// Language.Reflection.SourceLocation (65626)
| Idris_Language_Reflection_SourceLocation
/// Language.Reflection.SpecialName (65627)
| Idris_Language_Reflection_SpecialName
/// Language.Reflection.Str (4)
| Idris_Language_Reflection_Str
/// Prelude.Strings.StrCons (1)
| Idris_Prelude_Strings_StrCons
/// Prelude.Strings.StrM (65628)
| Idris_Prelude_Strings_StrM !Value
/// Prelude.Strings.StrNil (0)
| Idris_Prelude_Strings_StrNil
/// Language.Reflection.StrType (10)
| Idris_Language_Reflection_StrType
/// Prelude.Stream.Stream (65629)
| Idris_Prelude_Stream_Stream !Value
/// Language.Reflection.SubReport (4)
| Idris_Language_Reflection_SubReport
/// Prelude.Pairs.Subset (65630)
| Idris_Prelude_Pairs_Subset !Value !Value
/// Symbol_ (65631)
| Idris_Symbol_ !Value
/// Language.Reflection.TCon (3)
| Idris_Language_Reflection_TCon
/// Language.Reflection.TConst (4)
| Idris_Language_Reflection_TConst
/// Language.Reflection.TT (65632)
| Idris_Language_Reflection_TT
/// Language.Reflection.TTName (65633)
| Idris_Language_Reflection_TTName
/// Language.Reflection.TTUExp (65634)
| Idris_Language_Reflection_TTUExp
/// Language.Reflection.TType (6)
| Idris_Language_Reflection_TType
/// Language.Reflection.Tactic (65635)
| Idris_Language_Reflection_Tactic
/// Language.Reflection.TermPart (2)
| Idris_Language_Reflection_TermPart
/// Language.Reflection.TextPart (0)
| Idris_Language_Reflection_TextPart
/// TheWorld (0)
| Idris_TheWorld !Value
/// Language.Reflection.TheWorld (14)
| Idris_Language_Reflection_TheWorld
/// Language.Reflection.Errors.TooManyArguments (10)
| Idris_Language_Reflection_Errors_TooManyArguments
/// Prelude.Traversable.Traversable (65636)
| Idris_Prelude_Traversable_Traversable !Value
/// Language.Reflection.Trivial (6)
| Idris_Language_Reflection_Trivial
/// Prelude.Bool.True (1)
| Idris_Prelude_Bool_True
/// Language.Reflection.Try (0)
| Idris_Language_Reflection_Try
/// Language.Reflection.Elab.TyConArg (65637)
| Idris_Language_Reflection_Elab_TyConArg
/// Language.Reflection.Elab.TyConIndex (1)
| Idris_Language_Reflection_Elab_TyConIndex
/// Language.Reflection.Elab.TyConParameter (0)
| Idris_Language_Reflection_Elab_TyConParameter
/// Language.Reflection.Elab.TyDecl (65638)
| Idris_Language_Reflection_Elab_TyDecl
/// Language.Reflection.UN (0)
| Idris_Language_Reflection_UN
/// Builtins.UPair (65639)
| Idris_Builtins_UPair !Value !Value
/// Language.Reflection.UType (7)
| Idris_Language_Reflection_UType
/// Language.Reflection.UVal (1)
| Idris_Language_Reflection_UVal
/// Language.Reflection.UVar (0)
| Idris_Language_Reflection_UVar
/// Language.Reflection.Unfocus (5)
| Idris_Language_Reflection_Unfocus
/// Language.Reflection.Errors.UnifyScope (6)
| Idris_Language_Reflection_Errors_UnifyScope
/// Prelude.Uninhabited.Uninhabited (65640)
| Idris_Prelude_Uninhabited_Uninhabited !Value
/// Language.Reflection.UniqueType (1)
| Idris_Language_Reflection_UniqueType
/// Unit (65641)
| Idris_Unit
/// Language.Reflection.Universe (65642)
| Idris_Language_Reflection_Universe
/// Language.Reflection.Errors.UniverseError (23)
| Idris_Language_Reflection_Errors_UniverseError
/// Language.Reflection.Errors.UnknownImplicit (26)
| Idris_Language_Reflection_Errors_UnknownImplicit
/// Prelude.Show.User (4)
| Idris_Prelude_Show_User
/// Language.Reflection.V (1)
| Idris_Language_Reflection_V
/// Language.Reflection.Var (0)
| Idris_Language_Reflection_Var
/// Void (65643)
| Idris_Void
/// Language.Reflection.VoidType (11)
| Idris_Language_Reflection_VoidType
/// Prelude.WellFounded.WellFounded (65644)
| Idris_Prelude_WellFounded_WellFounded !Value !Value
/// Language.Reflection.WhereN (0)
| Idris_Language_Reflection_WhereN
/// Language.Reflection.Errors.WithFnType (13)
| Idris_Language_Reflection_Errors_WithFnType
/// Language.Reflection.WithN (1)
| Idris_Language_Reflection_WithN
/// World (65645)
| Idris_World
/// Language.Reflection.WorldType (13)
| Idris_Language_Reflection_WorldType
/// Prelude.File.WriteTruncate (1)
| Idris_Prelude_File_WriteTruncate
/// Prelude.Basics.Yes (0)
| Idris_Prelude_Basics_Yes
/// Prelude.Nat.Z (0)
| Idris_Prelude_Nat_Z
/// {__Infer0} (65646)
| Idris___Infer0
/// {__infer0} (0)
| Idris___infer0
/// {U_Prelude.Interactive.{putStr'0}1} (65647)
| Idris_U_Prelude_Interactive_putStr_39_01
/// {U_io_bind1} (65648)
| Idris_U_io_bind1 !Value !Value !Value !Value !Value
/// {U_io_pure1} (65649)
| Idris_U_io_pure1 !Value !Value !Value
/// {U_prim_write1} (65650)
| Idris_U_prim_write1 !Value !Value
/// {U_{io_bind1}1} (65651)
| Idris_U_io_bind11 !Value !Value !Value !Value !Value !Value
/// constructor of Prelude.Applicative.Alternative (0)
| Idris_Prelude_Applicative_Alternative_ictor
/// constructor of Prelude.Applicative.Applicative (0)
| Idris_Prelude_Applicative_Applicative_ictor
/// constructor of Prelude.Cast.Cast (0)
| Idris_Prelude_Cast_Cast_ictor
/// constructor of Decidable.Equality.DecEq (0)
| Idris_Decidable_Equality_DecEq_ictor
/// constructor of Prelude.Enum (0)
| Idris_Prelude_Enum_ictor
/// constructor of Prelude.Interfaces.Eq (0)
| Idris_Prelude_Interfaces_Eq_ictor
/// constructor of Prelude.Foldable.Foldable (0)
| Idris_Prelude_Foldable_Foldable_ictor
/// constructor of Prelude.Interfaces.Fractional (0)
| Idris_Prelude_Interfaces_Fractional_ictor
/// constructor of Prelude.Functor.Functor (0)
| Idris_Prelude_Functor_Functor_ictor
/// constructor of Prelude.Interfaces.Integral (0)
| Idris_Prelude_Interfaces_Integral_ictor
/// constructor of Prelude.Interfaces.MaxBound (0)
| Idris_Prelude_Interfaces_MaxBound_ictor
/// constructor of Prelude.Interfaces.MinBound (0)
| Idris_Prelude_Interfaces_MinBound_ictor
/// constructor of Prelude.Monad.Monad (0)
| Idris_Prelude_Monad_Monad_ictor
/// constructor of Prelude.Algebra.Monoid (0)
| Idris_Prelude_Algebra_Monoid_ictor
/// constructor of Prelude.Interfaces.Neg (0)
| Idris_Prelude_Interfaces_Neg_ictor
/// constructor of Prelude.Interfaces.Num (0)
| Idris_Prelude_Interfaces_Num_ictor
/// constructor of Prelude.Interfaces.Ord (0)
| Idris_Prelude_Interfaces_Ord_ictor
/// constructor of Language.Reflection.Quotable (0)
| Idris_Language_Reflection_Quotable_ictor
/// constructor of Language.Reflection.ReflConst (0)
| Idris_Language_Reflection_ReflConst_ictor
/// constructor of Prelude.Algebra.Semigroup (0)
| Idris_Prelude_Algebra_Semigroup_ictor
/// constructor of Prelude.Show.Show (0)
| Idris_Prelude_Show_Show_ictor
/// constructor of Prelude.Traversable.Traversable (0)
| Idris_Prelude_Traversable_Traversable_ictor
/// constructor of Prelude.Uninhabited.Uninhabited (0)
| Idris_Prelude_Uninhabited_Uninhabited_ictor
/// constructor of Prelude.WellFounded.WellFounded (0)
| Idris_Prelude_WellFounded_WellFounded_ictor
/// assert_unreachable
/// ____
idris_assert_unreachable :: Value
idris_assert_unreachable
= Nothing
/// call__IO
/// {APPLY0}(GLOB {e2}, ____)
idris_call__IO :: !Value !Value !Value -> Value
idris_call__IO e0 e1 e2
= (idris_APPLY0 e2 Nothing)
/// idris_crash
/// ____
idris_idris_crash :: Value
idris_idris_crash
= Nothing
/// io_bind
/// {APPLY0}({io_bind2}(GLOB {e0}, GLOB {e1}, GLOB {e2}, GLOB {e3}, GLOB {e4}, GLOB w), {APPLY0}(GLOB {e3}, GLOB w))
idris_io_bind :: !Value !Value !Value !Value !Value !Value -> Value
idris_io_bind e0 e1 e2 e3 e4 w
= (idris_APPLY0 (idris_io_bind2 e0 e1 e2 e3 e4 w) (idris_APPLY0 e3 w))
/// io_pure
/// GLOB {e2}
idris_io_pure :: !Value !Value !Value !Value -> Value
idris_io_pure e0 e1 e2 w
= e2
/// Main.main
/// Prelude.Interactive.putStr'(____, "Hello, Idris!\n")
idris_Main_main :: Value
idris_Main_main
= (idris_Prelude_Interactive_putStr_39_ Nothing (Boxed_String "Hello, Idris!\xa"))
/// mkForeignPrim
/// ____
idris_mkForeignPrim :: Value
idris_mkForeignPrim
= Nothing
/// prim__asPtr
/// LExternal prim__asPtr(GLOB {op0})
idris_prim__asPtr :: !Value -> Value
idris_prim__asPtr op0
= (abort "PRIMITIVE (LExternal prim__asPtr,[GLOB {op0}]) IS UNSUPPORTED")
/// prim__eqManagedPtr
/// LExternal prim__eqManagedPtr(GLOB {op0}, GLOB {op1})
idris_prim__eqManagedPtr :: !Value !Value -> Value
idris_prim__eqManagedPtr op0 op1
= (abort "PRIMITIVE (LExternal prim__eqManagedPtr,[GLOB {op0},GLOB {op1}]) IS UNSUPPORTED")
/// prim__eqPtr
/// LExternal prim__eqPtr(GLOB {op0}, GLOB {op1})
idris_prim__eqPtr :: !Value !Value -> Value
idris_prim__eqPtr op0 op1
= (abort "PRIMITIVE (LExternal prim__eqPtr,[GLOB {op0},GLOB {op1}]) IS UNSUPPORTED")
/// prim__null
/// LExternal prim__null()
idris_prim__null :: Value
idris_prim__null
= (abort "PRIMITIVE (LExternal prim__null,[]) IS UNSUPPORTED")
/// prim__peek16
/// LExternal prim__peek16(GLOB {op0}, GLOB {op1}, GLOB {op2})
idris_prim__peek16 :: !Value !Value !Value -> Value
idris_prim__peek16 op0 op1 op2
= (abort "PRIMITIVE (LExternal prim__peek16,[GLOB {op0},GLOB {op1},GLOB {op2}]) IS UNSUPPORTED")
/// prim__peek32
/// LExternal prim__peek32(GLOB {op0}, GLOB {op1}, GLOB {op2})
idris_prim__peek32 :: !Value !Value !Value -> Value
idris_prim__peek32 op0 op1 op2
= (abort "PRIMITIVE (LExternal prim__peek32,[GLOB {op0},GLOB {op1},GLOB {op2}]) IS UNSUPPORTED")
/// prim__peek64
/// LExternal prim__peek64(GLOB {op0}, GLOB {op1}, GLOB {op2})
idris_prim__peek64 :: !Value !Value !Value -> Value
idris_prim__peek64 op0 op1 op2
= (abort "PRIMITIVE (LExternal prim__peek64,[GLOB {op0},GLOB {op1},GLOB {op2}]) IS UNSUPPORTED")
/// prim__peek8
/// LExternal prim__peek8(GLOB {op0}, GLOB {op1}, GLOB {op2})
idris_prim__peek8 :: !Value !Value !Value -> Value
idris_prim__peek8 op0 op1 op2
= (abort "PRIMITIVE (LExternal prim__peek8,[GLOB {op0},GLOB {op1},GLOB {op2}]) IS UNSUPPORTED")
/// prim__peekDouble
/// LExternal prim__peekDouble(GLOB {op0}, GLOB {op1}, GLOB {op2})
idris_prim__peekDouble :: !Value !Value !Value -> Value
idris_prim__peekDouble op0 op1 op2
= (abort "PRIMITIVE (LExternal prim__peekDouble,[GLOB {op0},GLOB {op1},GLOB {op2}]) IS UNSUPPORTED")
/// prim__peekPtr
/// LExternal prim__peekPtr(GLOB {op0}, GLOB {op1}, GLOB {op2})
idris_prim__peekPtr :: !Value !Value !Value -> Value
idris_prim__peekPtr op0 op1 op2
= (abort "PRIMITIVE (LExternal prim__peekPtr,[GLOB {op0},GLOB {op1},GLOB {op2}]) IS UNSUPPORTED")
/// prim__peekSingle
/// LExternal prim__peekSingle(GLOB {op0}, GLOB {op1}, GLOB {op2})
idris_prim__peekSingle :: !Value !Value !Value -> Value
idris_prim__peekSingle op0 op1 op2
= (abort "PRIMITIVE (LExternal prim__peekSingle,[GLOB {op0},GLOB {op1},GLOB {op2}]) IS UNSUPPORTED")
/// prim__poke16
/// LExternal prim__poke16(GLOB {op0}, GLOB {op1}, GLOB {op2}, GLOB {op3})
idris_prim__poke16 :: !Value !Value !Value !Value -> Value
idris_prim__poke16 op0 op1 op2 op3
= (abort "PRIMITIVE (LExternal prim__poke16,[GLOB {op0},GLOB {op1},GLOB {op2},GLOB {op3}]) IS UNSUPPORTED")
/// prim__poke32
/// LExternal prim__poke32(GLOB {op0}, GLOB {op1}, GLOB {op2}, GLOB {op3})
idris_prim__poke32 :: !Value !Value !Value !Value -> Value
idris_prim__poke32 op0 op1 op2 op3
= (abort "PRIMITIVE (LExternal prim__poke32,[GLOB {op0},GLOB {op1},GLOB {op2},GLOB {op3}]) IS UNSUPPORTED")
/// prim__poke64
/// LExternal prim__poke64(GLOB {op0}, GLOB {op1}, GLOB {op2}, GLOB {op3})
idris_prim__poke64 :: !Value !Value !Value !Value -> Value
idris_prim__poke64 op0 op1 op2 op3
= (abort "PRIMITIVE (LExternal prim__poke64,[GLOB {op0},GLOB {op1},GLOB {op2},GLOB {op3}]) IS UNSUPPORTED")
/// prim__poke8
/// LExternal prim__poke8(GLOB {op0}, GLOB {op1}, GLOB {op2}, GLOB {op3})
idris_prim__poke8 :: !Value !Value !Value !Value -> Value
idris_prim__poke8 op0 op1 op2 op3
= (abort "PRIMITIVE (LExternal prim__poke8,[GLOB {op0},GLOB {op1},GLOB {op2},GLOB {op3}]) IS UNSUPPORTED")
/// prim__pokeDouble
/// LExternal prim__pokeDouble(GLOB {op0}, GLOB {op1}, GLOB {op2}, GLOB {op3})
idris_prim__pokeDouble :: !Value !Value !Value !Value -> Value
idris_prim__pokeDouble op0 op1 op2 op3
= (abort "PRIMITIVE (LExternal prim__pokeDouble,[GLOB {op0},GLOB {op1},GLOB {op2},GLOB {op3}]) IS UNSUPPORTED")
/// prim__pokePtr
/// LExternal prim__pokePtr(GLOB {op0}, GLOB {op1}, GLOB {op2}, GLOB {op3})
idris_prim__pokePtr :: !Value !Value !Value !Value -> Value
idris_prim__pokePtr op0 op1 op2 op3
= (abort "PRIMITIVE (LExternal prim__pokePtr,[GLOB {op0},GLOB {op1},GLOB {op2},GLOB {op3}]) IS UNSUPPORTED")
/// prim__pokeSingle
/// LExternal prim__pokeSingle(GLOB {op0}, GLOB {op1}, GLOB {op2}, GLOB {op3})
idris_prim__pokeSingle :: !Value !Value !Value !Value -> Value
idris_prim__pokeSingle op0 op1 op2 op3
= (abort "PRIMITIVE (LExternal prim__pokeSingle,[GLOB {op0},GLOB {op1},GLOB {op2},GLOB {op3}]) IS UNSUPPORTED")
/// prim__ptrOffset
/// LExternal prim__ptrOffset(GLOB {op0}, GLOB {op1})
idris_prim__ptrOffset :: !Value !Value -> Value
idris_prim__ptrOffset op0 op1
= (abort "PRIMITIVE (LExternal prim__ptrOffset,[GLOB {op0},GLOB {op1}]) IS UNSUPPORTED")
/// prim__readFile
/// LExternal prim__readFile(GLOB {op0}, GLOB {op1})
idris_prim__readFile :: !Value !Value -> Value
idris_prim__readFile op0 op1
= (abort "PRIMITIVE (LExternal prim__readFile,[GLOB {op0},GLOB {op1}]) IS UNSUPPORTED")
/// prim__registerPtr
/// LExternal prim__registerPtr(GLOB {op0}, GLOB {op1})
idris_prim__registerPtr :: !Value !Value -> Value
idris_prim__registerPtr op0 op1
= (abort "PRIMITIVE (LExternal prim__registerPtr,[GLOB {op0},GLOB {op1}]) IS UNSUPPORTED")
/// prim__sizeofPtr
/// LExternal prim__sizeofPtr()
idris_prim__sizeofPtr :: Value
idris_prim__sizeofPtr
= (abort "PRIMITIVE (LExternal prim__sizeofPtr,[]) IS UNSUPPORTED")
/// prim__stderr
/// LExternal prim__stderr()
idris_prim__stderr :: Value
idris_prim__stderr
= (abort "PRIMITIVE (LExternal prim__stderr,[]) IS UNSUPPORTED")
/// prim__stdin
/// LExternal prim__stdin()
idris_prim__stdin :: Value
idris_prim__stdin
= (abort "PRIMITIVE (LExternal prim__stdin,[]) IS UNSUPPORTED")
/// prim__stdout
/// LExternal prim__stdout()
idris_prim__stdout :: Value
idris_prim__stdout
= (abort "PRIMITIVE (LExternal prim__stdout,[]) IS UNSUPPORTED")
/// prim__vm
/// LExternal prim__vm(GLOB {op0})
idris_prim__vm :: !Value -> Value
idris_prim__vm op0
= (abort "PRIMITIVE (LExternal prim__vm,[GLOB {op0}]) IS UNSUPPORTED")
/// prim__writeFile
/// LExternal prim__writeFile(GLOB {op0}, GLOB {op1}, GLOB {op2})
idris_prim__writeFile :: !Value !Value !Value -> Value
idris_prim__writeFile op0 op1 op2
= (abort "PRIMITIVE (LExternal prim__writeFile,[GLOB {op0},GLOB {op1},GLOB {op2}]) IS UNSUPPORTED")
/// prim__writeString
/// LWriteStr(GLOB {op0}, GLOB {op1})
idris_prim__writeString :: !Value !Value -> Value
idris_prim__writeString op0 op1
= (clean_System_write_String op0 op1)
/// prim_io_bind
/// {APPLY0}(GLOB {e3}, GLOB {e2})
idris_prim_io_bind :: !Value !Value !Value !Value -> Value
idris_prim_io_bind e0 e1 e2 e3
= (idris_APPLY0 e3 e2)
/// prim_write
/// LWriteStr(GLOB w, GLOB {e1})
idris_prim_write :: !Value !Value !Value -> Value
idris_prim_write e0 e1 w
= (clean_System_write_String w e1)
/// Prelude.Interactive.putStr'
/// {U_io_bind1}(____, ____, ____, {U_prim_write1}(____, GLOB {e1}), {U_Prelude.Interactive.{putStr'0}1}())
idris_Prelude_Interactive_putStr_39_ :: !Value !Value -> Value
idris_Prelude_Interactive_putStr_39_ e0 e1
= (Idris_U_io_bind1 Nothing Nothing Nothing (Idris_U_prim_write1 Nothing e1) (Idris_U_Prelude_Interactive_putStr_39_01))
/// run__IO
/// {APPLY0}(GLOB {e1}, ____)
idris_run__IO :: !Value !Value -> Value
idris_run__IO e0 e1
= (idris_APPLY0 e1 Nothing)
/// unsafePerformPrimIO
/// ____
idris_unsafePerformPrimIO :: Value
idris_unsafePerformPrimIO
= Nothing
/// world
/// GLOB {e0}
idris_world :: !Value -> Value
idris_world e0
= e0
/// {APPLY0}
/// case' GLOB {fn0} of { {U_Prelude.Interactive.{putStr'0}1}() => Prelude.Interactive.{putStr'0}(GLOB {arg0}) | {U_io_bind1}({P_c0}, {P_c1}, {P_c2}, {P_c3}, {P_c4}) => io_bind(GLOB {P_c0}, GLOB {P_c1}, GLOB {P_c2}, GLOB {P_c3}, GLOB {P_c4}, GLOB {arg0}) | {U_io_pure1}({P_c0}, {P_c1}, {P_c2}) => io_pure(GLOB {P_c0}, GLOB {P_c1}, GLOB {P_c2}, GLOB {arg0}) | {U_prim_write1}({P_c0}, {P_c1}) => prim_write(GLOB {P_c0}, GLOB {P_c1}, GLOB {arg0}) | {U_{io_bind1}1}({P_c0}, {P_c1}, {P_c2}, {P_c3}, {P_c4}, {P_c5}) => {io_bind1}(GLOB {P_c0}, GLOB {P_c1}, GLOB {P_c2}, GLOB {P_c3}, GLOB {P_c4}, GLOB {P_c5}, GLOB {arg0}) | _ => ____
idris_APPLY0 :: !Value !Value -> Value
idris_APPLY0 fn0 arg0
= (case fn0 of
Idris_U_Prelude_Interactive_putStr_39_01 -> (idris_Prelude_Interactive_putStr_39_0 arg0)
Idris_U_io_bind1 p_c0 p_c1 p_c2 p_c3 p_c4 -> (idris_io_bind p_c0 p_c1 p_c2 p_c3 p_c4 arg0)
Idris_U_io_pure1 p_c0 p_c1 p_c2 -> (idris_io_pure p_c0 p_c1 p_c2 arg0)
Idris_U_prim_write1 p_c0 p_c1 -> (idris_prim_write p_c0 p_c1 arg0)
Idris_U_io_bind11 p_c0 p_c1 p_c2 p_c3 p_c4 p_c5 -> (idris_io_bind1 p_c0 p_c1 p_c2 p_c3 p_c4 p_c5 arg0)
_ -> Nothing)
/// {APPLY20}
/// ____
idris_APPLY20 :: !Value !Value !Value -> Value
idris_APPLY20 fn0 arg00 arg10
= Nothing
/// {EVAL0}
/// case' GLOB {arg0} of { _ => GLOB {arg0}
idris_EVAL0 :: !Value -> Value
idris_EVAL0 arg0
= (case arg0 of
_ -> arg0)
/// {io_bind0}
/// {APPLY0}(GLOB {e4}, GLOB {in0})
idris_io_bind0 :: !Value !Value !Value !Value !Value !Value !Value -> Value
idris_io_bind0 e0 e1 e2 e3 e4 w in0
= (idris_APPLY0 e4 in0)
/// Prelude.Interactive.{putStr'0}
/// {U_io_pure1}(____, ____, CON MkUnit())
idris_Prelude_Interactive_putStr_39_0 :: !Value -> Value
idris_Prelude_Interactive_putStr_39_0 in0
= (Idris_U_io_pure1 Nothing Nothing (Idris_MkUnit))
/// {runMain0}
/// {EVAL0}({APPLY0}(Main.main(), ____))
idris_runMain0 :: Value
idris_runMain0
= (idris_EVAL0 (idris_APPLY0 (idris_Main_main) Nothing))
/// {io_bind1}
/// {APPLY0}({io_bind0}(GLOB {e0}, GLOB {e1}, GLOB {e2}, GLOB {e3}, GLOB {e4}, GLOB w, GLOB {in0}), GLOB w)
idris_io_bind1 :: !Value !Value !Value !Value !Value !Value !Value -> Value
idris_io_bind1 e0 e1 e2 e3 e4 w in0
= (idris_APPLY0 (idris_io_bind0 e0 e1 e2 e3 e4 w in0) w)
/// {io_bind2}
/// {U_{io_bind1}1}(GLOB {e0}, GLOB {e1}, GLOB {e2}, GLOB {e3}, GLOB {e4}, GLOB w)
idris_io_bind2 :: !Value !Value !Value !Value !Value !Value -> Value
idris_io_bind2 e0 e1 e2 e3 e4 w
= (Idris_U_io_bind11 e0 e1 e2 e3 e4 w)
/// Decidable.Equality.Decidable.Equality.Char implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq
/// ____
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_Char_58__33_decEq_58_0_58_primitiveNotEq_58_0 :: Value
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_Char_58__33_decEq_58_0_58_primitiveNotEq_58_0
= Nothing
/// Decidable.Equality.Decidable.Equality.Int implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq
/// ____
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_Int_58__33_decEq_58_0_58_primitiveNotEq_58_0 :: Value
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_Int_58__33_decEq_58_0_58_primitiveNotEq_58_0
= Nothing
/// Decidable.Equality.Decidable.Equality.Integer implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq
/// ____
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_Integer_58__33_decEq_58_0_58_primitiveNotEq_58_0 :: Value
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_Integer_58__33_decEq_58_0_58_primitiveNotEq_58_0
= Nothing
/// Decidable.Equality.Decidable.Equality.ManagedPtr implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq
/// ____
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_ManagedPtr_58__33_decEq_58_0_58_primitiveNotEq_58_0 :: Value
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_ManagedPtr_58__33_decEq_58_0_58_primitiveNotEq_58_0
= Nothing
/// Decidable.Equality.Decidable.Equality.Ptr implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq
/// ____
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_Ptr_58__33_decEq_58_0_58_primitiveNotEq_58_0 :: Value
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_Ptr_58__33_decEq_58_0_58_primitiveNotEq_58_0
= Nothing
/// Decidable.Equality.Decidable.Equality.String implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq
/// ____
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_String_58__33_decEq_58_0_58_primitiveNotEq_58_0 :: Value
idris_Decidable_Equality_Decidable_Equality__64_Decidable_Equality_DecEq_36_String_58__33_decEq_58_0_58_primitiveNotEq_58_0
= Nothing
/// case block in io_bind at IO.idr:107:34
/// {APPLY0}(GLOB {e7}, GLOB {e5})
idris_io_bind_IO__idr_107_34_case :: !Value !Value !Value !Value !Value !Value !Value !Value -> Value
idris_io_bind_IO__idr_107_34_case e0 e1 e2 e3 e4 e5 e6 e7
= (idris_APPLY0 e7 e5)
/// case block in Void at (casefun Void)
/// ____
idris_Void___casefun__Void___case :: Value
idris_Void___casefun__Void___case
= Nothing
/// <<Void eliminator>>
/// ____
idris_Void_elim :: Value
idris_Void_elim
= Nothing
Start = idris_runMain0
/*
--- ForeignEnv.:: ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 5, nt_unique = False} {xs : Prelude.List.List Type ./IO.idr.h16} -> {t : Type ./IO.idr.j16} -> {f : FFI} -> Builtins.Pair (FFI.ffi_types f t) t -> ForeignEnv.FEnv f xs -> ForeignEnv.FEnv f (Prelude.List.:: Type ./IO.idr.p16 t xs)
--- Prelude.List.:: ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 3, nt_unique = False} {elem : Type ./Prelude/List.idr.c1} -> elem -> Prelude.List.List elem -> Prelude.List.List elem
--- Prelude.Stream.:: ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {elem : Type ./Prelude/Stream.idr.z} -> elem -> Inf (Prelude.Stream.Stream elem) -> Prelude.Stream.Stream elem
--- = ---
RigCount: RigW
Injectivity: True
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: DataMI [0,2]
---
TyDecl: TCon {nt_tag = 7, nt_arity = 4} {A : Type primitive.g} -> {B : Type primitive.j} -> A -> B -> Type primitive.o
--- Language.Reflection.ATDouble ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Language.Reflection.ArithTy
--- Language.Reflection.ATInt ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Language.Reflection.IntTy -> Language.Reflection.ArithTy
--- Language.Reflection.AType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 9, nt_arity = 1, nt_unique = False} Language.Reflection.ArithTy -> Language.Reflection.Const
--- Prelude.WellFounded.Access ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {a : Type ./Prelude/WellFounded.idr.f1} -> {x : a} -> {rel : a -> a -> Type ./Prelude/WellFounded.idr.l1} -> ((y : a) -> rel y x -> Prelude.WellFounded.Accessible a rel y) -> Prelude.WellFounded.Accessible a rel x
--- Prelude.WellFounded.Accessible ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 3} {a : Type ./Prelude/WellFounded.idr.u} -> (a -> a -> Type ./Prelude/WellFounded.idr.z) -> a -> Type ./Prelude/WellFounded.idr.d1
--- Prelude.Nat.Additive ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 114, nt_arity = 0} Type ./Prelude/Nat.idr.z28
--- Language.Reflection.AllTypes ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Language.Reflection.Universe
--- Language.Reflection.Errors.AlreadyDefined ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 28, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Prelude.Applicative.Alternative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 17, nt_arity = 1} (Type ./Prelude/Applicative.idr.y24 -> Type ./Prelude/Applicative.idr.b25) -> Type ./Prelude/Applicative.idr.e25
--- Language.Reflection.App ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 2, nt_unique = False} Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.TT
--- Prelude.Show.App ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 0, nt_unique = False} Prelude.Show.Prec
--- Prelude.File.Append ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Prelude.File.Mode
--- Prelude.Applicative.Applicative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} (Type ./Prelude/Applicative.idr.u -> Type ./Prelude/Applicative.idr.x) -> Type ./Prelude/Applicative.idr.a1
--- Language.Reflection.ApplyTactic ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 12, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Tactic
--- Language.Reflection.ArithTy ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 273, nt_arity = 0} Type ./Language/Reflection.idr.c137
--- Language.Reflection.B16 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 1, nt_unique = False} Bits16 -> Language.Reflection.Const
--- Language.Reflection.B32 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 7, nt_arity = 1, nt_unique = False} Bits32 -> Language.Reflection.Const
--- Language.Reflection.B64 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 8, nt_arity = 1, nt_unique = False} Bits64 -> Language.Reflection.Const
--- Language.Reflection.B8 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 1, nt_unique = False} Bits8 -> Language.Reflection.Const
--- Language.Reflection.BI ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} Integer -> Language.Reflection.Const
--- Prelude.Show.Backtick ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} Prelude.Show.Prec
--- Language.Reflection.Bind ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 3, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Binder Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.TT
--- Language.Reflection.Binder ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 297, nt_arity = 1} Type ./Language/Reflection.idr.w140 -> Type ./Language/Reflection.idr.z140
--- Prelude.Bool.Bool ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 0} Type ./Prelude/Bool.idr.u
--- Ownership.Borrowed ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 31, nt_arity = 1} UniqueType -> NullType
--- Language.Reflection.Bound ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Language.Reflection.NameType
--- Language.Reflection.ByReflection ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 14, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Tactic
--- CData ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 0, nt_arity = 0} Type ./Builtins.idr.d29
--- FFI_C.CFnPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 45, nt_arity = 1} Type ./IO.idr.q38 -> Type ./IO.idr.t38
--- FFI_C.C_Any ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 1, nt_unique = False} {a : Type ./IO.idr.g45} -> FFI_C.C_Types (FFI_C.Raw a)
--- FFI_C.C_CData ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 8, nt_arity = 0, nt_unique = False} FFI_C.C_Types CData
--- FFI_C.C_Float ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} FFI_C.C_Types Double
--- FFI_C.C_Fn ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {t : Type ./IO.idr.e42} -> {s : Type ./IO.idr.h42} -> FFI_C.C_Types s -> FFI_C.C_FnTypes t -> FFI_C.C_FnTypes (s -> t)
--- FFI_C.C_FnBase ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 2, nt_unique = False} {t : Type ./IO.idr.r42} -> FFI_C.C_Types t -> FFI_C.C_FnTypes t
--- FFI_C.C_FnIO ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not strictly positive
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} {t : Type ./IO.idr.n42} -> FFI_C.C_Types t -> FFI_C.C_FnTypes (IO' FFI_C.FFI_C t)
--- FFI_C.C_FnT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 2, nt_unique = False} {t : Type ./IO.idr.j45} -> FFI_C.C_FnTypes t -> FFI_C.C_Types (FFI_C.CFnPtr t)
--- FFI_C.C_FnTypes ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 48, nt_arity = 1} Type ./IO.idr.z41 -> Type ./IO.idr.c42
--- FFI_C.C_IntBits16 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} FFI_C.C_IntTypes Bits16
--- FFI_C.C_IntBits32 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 0, nt_unique = False} FFI_C.C_IntTypes Bits32
--- FFI_C.C_IntBits64 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 0, nt_unique = False} FFI_C.C_IntTypes Bits64
--- FFI_C.C_IntBits8 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} FFI_C.C_IntTypes Bits8
--- FFI_C.C_IntChar ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} FFI_C.C_IntTypes Char
--- FFI_C.C_IntNative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} FFI_C.C_IntTypes Int
--- FFI_C.C_IntT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 7, nt_arity = 2, nt_unique = False} {i : Type ./IO.idr.n45} -> FFI_C.C_IntTypes i -> FFI_C.C_Types i
--- FFI_C.C_IntTypes ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 46, nt_arity = 1} Type ./IO.idr.o39 -> Type ./IO.idr.r39
--- FFI_C.C_MPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} FFI_C.C_Types ManagedPtr
--- FFI_C.C_Ptr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} FFI_C.C_Types Ptr
--- FFI_C.C_Str ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} FFI_C.C_Types String
--- FFI_C.C_Types ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 50, nt_arity = 1} Type ./IO.idr.b45 -> Type ./IO.idr.e45
--- FFI_C.C_Unit ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 0, nt_unique = False} FFI_C.C_Types Unit
--- Language.Reflection.Errors.CantConvert ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 3, nt_unique = False} Language.Reflection.TT -> Language.Reflection.TT -> Prelude.List.List (Builtins.Pair Language.Reflection.TTName Language.Reflection.TT) -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.CantInferType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 7, nt_arity = 1, nt_unique = False} String -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.CantIntroduce ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 11, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.CantMatch ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 14, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.CantResolve ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 17, nt_arity = 2, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Errors.Err -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.CantResolveAlts ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 19, nt_arity = 1, nt_unique = False} Prelude.List.List Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.CantSolveGoal ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 2, nt_unique = False} Language.Reflection.TT -> Prelude.List.List (Builtins.Pair Language.Reflection.TTName Language.Reflection.TT) -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.CantUnify ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 6, nt_unique = False} Prelude.Bool.Bool -> Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.Errors.Err -> Prelude.List.List (Builtins.Pair Language.Reflection.TTName Language.Reflection.TT) -> Int -> Language.Reflection.Errors.Err
--- Language.Reflection.Case ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 20, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Tactic
--- Language.Reflection.CaseN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 2, nt_unique = False} Language.Reflection.SourceLocation -> Language.Reflection.TTName -> Language.Reflection.SpecialName
--- Prelude.Cast.Cast ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 2} Type ./Prelude/Cast.idr.u -> Type ./Prelude/Cast.idr.x -> Type ./Prelude/Cast.idr.a1
--- Language.Reflection.Ch ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 1, nt_unique = False} Char -> Language.Reflection.Const
--- Language.Reflection.Claim ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TT -> Language.Reflection.Tactic
--- Prelude.Nat.CmpEQ ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} {x : Prelude.Nat.Nat} -> Prelude.Nat.CmpNat x x
--- Prelude.Nat.CmpGT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 2, nt_unique = False} {y : Prelude.Nat.Nat} -> (x : Prelude.Nat.Nat) -> Prelude.Nat.CmpNat (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num y (Prelude.Nat.S x)) y
--- Prelude.Nat.CmpLT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {x : Prelude.Nat.Nat} -> (y : Prelude.Nat.Nat) -> Prelude.Nat.CmpNat x (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num x (Prelude.Nat.S y))
--- Prelude.Nat.CmpNat ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 177, nt_arity = 2} Prelude.Nat.Nat -> Prelude.Nat.Nat -> Type ./Prelude/Nat.idr.y42
--- Language.Reflection.Compute ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 23, nt_arity = 0, nt_unique = False} Language.Reflection.Tactic
--- Language.Reflection.Const ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 274, nt_arity = 0} Type ./Language/Reflection.idr.f137
--- Language.Reflection.Elab.Constraint ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Plicity
--- Language.Reflection.Elab.Constructor ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} Language.Reflection.TTName -> Prelude.List.List Language.Reflection.Elab.FunArg -> Language.Reflection.Raw -> Language.Reflection.Elab.ConstructorDefn
--- Language.Reflection.Elab.ConstructorDefn ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 35, nt_arity = 0} Type ./Language/Reflection/Elab.idr.p12
--- Language.Reflection.Elab.CtorArg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 47, nt_arity = 0} Type ./Language/Reflection/Elab.idr.m16
--- Language.Reflection.Elab.CtorField ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} Language.Reflection.Elab.FunArg -> Language.Reflection.Elab.CtorArg
--- Language.Reflection.Elab.CtorParameter ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Language.Reflection.Elab.FunArg -> Language.Reflection.Elab.CtorArg
--- Language.Reflection.DCon ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 2, nt_unique = False} Int -> Int -> Language.Reflection.NameType
--- FFI_Export.DHere ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} ({phTy0} : Type ./IO.idr.g60) -> {t : {phTy0}} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.k60 {phTy0})} -> {x : Type ./IO.idr.m60} -> FFI_Export.DataDefined {phTy0} x (Prelude.List.:: (Builtins.Pair Type ./IO.idr.p60 {phTy0}) (Builtins.MkPair Type ./IO.idr.q60 {phTy0} x t) xs) t
--- Builtins.DPair ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 15, nt_arity = 2} (a : Type ./Builtins.idr.w7) -> (a -> Type ./Builtins.idr.a8) -> Type ./Builtins.idr.d8
--- FFI_Export.DThere ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 6, nt_unique = False} ({phTy0} : Type ./IO.idr.r60) -> {t : {phTy0}} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.v60 {phTy0})} -> {y : Builtins.Pair Type ./IO.idr.x60 {phTy0}} -> {x : Type ./IO.idr.z60} -> FFI_Export.DataDefined {phTy0} x xs t -> FFI_Export.DataDefined {phTy0} x (Prelude.List.:: (Builtins.Pair Type ./IO.idr.d61 {phTy0}) y xs) t
--- FFI_Export.Data ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 6, nt_unique = False} {h : String} -> {f : FFI} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.n67 (FFI.ffi_data f))} -> (x : Type ./IO.idr.p67) -> (n : FFI.ffi_data f) -> FFI_Export.FFI_Export f h (Prelude.List.:: (Builtins.Pair Type ./IO.idr.t67 (FFI.ffi_data f)) (Builtins.MkPair Type ./IO.idr.u67 (FFI.ffi_data f) x n) xs) -> FFI_Export.FFI_Export f h xs
--- FFI_Export.DataDefined ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 69, nt_arity = 4} {s : Type ./IO.idr.v59} -> Type ./IO.idr.y59 -> Prelude.List.List (Builtins.Pair Type ./IO.idr.b60 s) -> s -> Type ./IO.idr.e60
--- Language.Reflection.Elab.DataDefn ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 42, nt_arity = 0} Type ./Language/Reflection/Elab.idr.c15
--- Language.Reflection.Elab.Datatype ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 48, nt_arity = 0} Type ./Language/Reflection/Elab.idr.q16
--- Prelude.Basics.Dec ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 18, nt_arity = 1} Type ./Prelude/Basics.idr.h13 -> Type ./Prelude/Basics.idr.k13
--- Decidable.Equality.DecEq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 9, nt_arity = 1} Type ./Decidable/Equality.idr.a2 -> Type ./Decidable/Equality.idr.d2
--- Language.Reflection.Elab.Declare ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} Language.Reflection.TTName -> Prelude.List.List Language.Reflection.Elab.FunArg -> Language.Reflection.Raw -> Language.Reflection.Elab.TyDecl
--- Language.Reflection.Elab.DefineDatatype ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Prelude.List.List Language.Reflection.Elab.ConstructorDefn -> Language.Reflection.Elab.DataDefn
--- Language.Reflection.Elab.DefineFun ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {a : Type ./Language/Reflection/Elab.idr.m8} -> Language.Reflection.TTName -> Prelude.List.List (Language.Reflection.Elab.FunClause a) -> Language.Reflection.Elab.FunDefn a
--- Delay ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {t : DelayReason} -> {a : Type ./Builtins.idr.c21} -> a -> Delayed t a
--- DelayReason ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 26, nt_arity = 0} Type ./Builtins.idr.t20
--- Delayed ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 27, nt_arity = 2} DelayReason -> Type ./Builtins.idr.w20 -> Type ./Builtins.idr.z20
--- Prelude.Show.Dollar ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Prelude.Show.Prec
--- Prelude.Interfaces.EQ ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Prelude.Interfaces.Ordering
--- Prelude.Either.Either ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 2} Type ./Prelude/Either.idr.u -> Type ./Prelude/Either.idr.x -> Type ./Prelude/Either.idr.a1
--- Language.Reflection.Elab.Elab ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 57, nt_arity = 1} Type ./Language/Reflection/Elab.idr.o20 -> Type ./Language/Reflection/Elab.idr.r20
--- Prelude.Pairs.Element ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {a : Type ./Prelude/Pairs.idr.z2} -> {P : a -> Type ./Prelude/Pairs.idr.d3} -> (x : a) -> P x -> Prelude.Pairs.Subset a P
--- Language.Reflection.ElimN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.SpecialName
--- FFI_Export.End ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 3, nt_unique = False} {h : String} -> {f : FFI} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.j68 (FFI.ffi_data f))} -> FFI_Export.FFI_Export f h xs
--- Prelude.Enum ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 83, nt_arity = 1} Type ./Prelude.idr.y56 -> Type ./Prelude.idr.b57
--- Prelude.Interfaces.Eq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 11, nt_arity = 1} Type ./Prelude/Interfaces.idr.e2 -> Type ./Prelude/Interfaces.idr.h2
--- Prelude.Show.Eq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Prelude.Show.Prec
--- Language.Reflection.Elab.Erased ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Erasure
--- Language.Reflection.Erased ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 0, nt_unique = False} Language.Reflection.TT
--- Language.Reflection.Elab.Erasure ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 9, nt_arity = 0} Type ./Language/Reflection/Elab.idr.a1
--- Language.Reflection.Errors.Err ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 0} Type ./Language/Reflection/Errors.idr.u
--- Prelude.Providers.Error ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} {a : Type ./Prelude/Providers.idr.d1} -> String -> Prelude.Providers.Provider a
--- Language.Reflection.ErrorReportPart ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 329, nt_arity = 0} Type ./Language/Reflection.idr.j173
--- Prelude.Pairs.Evidence ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {a : Type ./Prelude/Pairs.idr.h2} -> {P : a -> Type ./Prelude/Pairs.idr.l2} -> (x : a) -> P x -> Prelude.Pairs.Exists a P
--- Language.Reflection.Exact ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 16, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Tactic
--- Prelude.Pairs.Exists ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 9, nt_arity = 2} {a : Type ./Prelude/Pairs.idr.y1} -> (a -> Type ./Prelude/Pairs.idr.c2) -> Type ./Prelude/Pairs.idr.f2
--- Language.Reflection.Elab.Explicit ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Plicity
--- ForeignEnv.FEnv ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 22, nt_arity = 2} FFI -> Prelude.List.List Type ./IO.idr.b16 -> Type ./IO.idr.d16
--- FFI ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 12, nt_arity = 0} Type ./IO.idr.a2
--- FFI_Export.FFI_Base ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 71, nt_arity = 3} (f : FFI) -> Prelude.List.List (Builtins.Pair Type ./IO.idr.b65 (FFI.ffi_data f)) -> Type ./IO.idr.d65 -> Type ./IO.idr.g65
--- FFI_Export.FFI_ExpType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 5, nt_unique = False} {t : Type ./IO.idr.i65} -> {f : FFI} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.m65 (FFI.ffi_data f))} -> {n : FFI.ffi_data f} -> FFI_Export.DataDefined (FFI.ffi_data f) t xs n -> FFI_Export.FFI_Base f xs t
--- FFI_Export.FFI_Export ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 73, nt_arity = 3} (f : FFI) -> String -> Prelude.List.List (Builtins.Pair Type ./IO.idr.h67 (FFI.ffi_data f)) -> Type ./IO.idr.j67
--- FFI_Export.FFI_Exportable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 72, nt_arity = 3} (f : FFI) -> Prelude.List.List (Builtins.Pair Type ./IO.idr.y65 (FFI.ffi_data f)) -> Type ./IO.idr.a66 -> Type ./IO.idr.d66
--- FFI_Export.FFI_Fun ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 6, nt_unique = False} {t : Type ./IO.idr.m66} -> {s : Type ./IO.idr.p66} -> {f : FFI} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.t66 (FFI.ffi_data f))} -> FFI_Export.FFI_Base f xs s -> FFI_Export.FFI_Exportable f xs t -> FFI_Export.FFI_Exportable f xs (s -> t)
--- FFI_Export.FFI_IO ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {t : Type ./IO.idr.f66} -> {f : FFI} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.j66 (FFI.ffi_data f))} -> FFI_Export.FFI_Base f xs t -> FFI_Export.FFI_Exportable f xs (IO' f t)
--- FFI_Export.FFI_Prim ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 4, nt_unique = False} {t : Type ./IO.idr.q65} -> {f : FFI} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.u65 (FFI.ffi_data f))} -> FFI.ffi_types f t -> FFI_Export.FFI_Base f xs t
--- FFI_Export.FFI_Ret ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 4, nt_unique = False} {t : Type ./IO.idr.y66} -> {f : FFI} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.c67 (FFI.ffi_data f))} -> FFI_Export.FFI_Base f xs t -> FFI_Export.FFI_Exportable f xs t
--- FFun ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 6, nt_unique = False} {t : Type ./IO.idr.d12} -> {s : Type ./IO.idr.g12} -> {xs : Prelude.List.List Type ./IO.idr.j12} -> {f : FFI} -> FFI.ffi_types f s -> FTy f (Prelude.List.:: Type ./IO.idr.n12 s xs) t -> FTy f xs (s -> t)
--- Prelude.File.FHandle ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Ptr -> Prelude.File.File
--- FRet ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {t : Type ./IO.idr.w11} -> {f : FFI} -> {xs : Prelude.List.List Type ./IO.idr.a12} -> FFI.ffi_types f t -> FTy f xs (IO' f t)
--- FTy ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 20, nt_arity = 3} FFI -> Prelude.List.List Type ./IO.idr.p11 -> Type ./IO.idr.r11 -> Type ./IO.idr.u11
--- Language.Reflection.Fail ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 25, nt_arity = 1, nt_unique = False} Prelude.List.List Language.Reflection.ErrorReportPart -> Language.Reflection.Tactic
--- Prelude.Bool.False ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Prelude.Bool.Bool
--- Prelude.File.File ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 0} Type ./Prelude/File.idr.u
--- Prelude.File.FileError ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 9, nt_arity = 0} Type ./Prelude/File.idr.x
--- Language.Reflection.FileLoc ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} String -> Builtins.Pair Int Int -> Builtins.Pair Int Int -> Language.Reflection.SourceLocation
--- Prelude.File.FileNotFound ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} Prelude.File.FileError
--- Prelude.File.FileReadError ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Prelude.File.FileError
--- Prelude.File.FileWriteError ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Prelude.File.FileError
--- Language.Reflection.Fill ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 15, nt_arity = 1, nt_unique = False} Language.Reflection.Raw -> Language.Reflection.Tactic
--- Language.Reflection.Elab.Fixity ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 0} Type ./Language/Reflection/Elab.idr.u
--- Language.Reflection.Fl ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 1, nt_unique = False} Double -> Language.Reflection.Const
--- Language.Reflection.Focus ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 17, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Tactic
--- Prelude.Foldable.Foldable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} (Type ./Prelude/Foldable.idr.u -> Type ./Prelude/Foldable.idr.x) -> Type ./Prelude/Foldable.idr.a1
--- Language.Reflection.Forgot ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 12, nt_arity = 0, nt_unique = False} Language.Reflection.Const
--- Prelude.Interfaces.Fractional ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 296, nt_arity = 1} Type ./Prelude/Interfaces.idr.r123 -> Type ./Prelude/Interfaces.idr.u123
--- FFI_Export.Fun ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 8, nt_unique = False} {h : String} -> {f : FFI} -> {xs : Prelude.List.List (Builtins.Pair Type ./IO.idr.y67 (FFI.ffi_data f))} -> {t : Type ./IO.idr.a68} -> t -> FFI.ffi_fn f -> FFI_Export.FFI_Exportable f xs t -> FFI_Export.FFI_Export f h xs -> FFI_Export.FFI_Export f h xs
--- Language.Reflection.Elab.FunArg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 11, nt_arity = 0} Type ./Language/Reflection/Elab.idr.e1
--- Language.Reflection.Elab.FunClause ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 28, nt_arity = 1} Type ./Language/Reflection/Elab.idr.t7 -> Type ./Language/Reflection/Elab.idr.w7
--- Language.Reflection.Elab.FunDefn ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 29, nt_arity = 1} Type ./Language/Reflection/Elab.idr.h8 -> Type ./Language/Reflection/Elab.idr.k8
--- Prelude.Functor.Functor ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} (Type ./Prelude/Functor.idr.u -> Type ./Prelude/Functor.idr.x) -> Type ./Prelude/Functor.idr.a1
--- Language.Reflection.GHole ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection.idr.t141} -> a -> Language.Reflection.Binder a
--- Prelude.Interfaces.GT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Prelude.Interfaces.Ordering
--- Prelude.File.GenericFileError ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Int -> Prelude.File.FileError
--- Prelude.Nat.GetAdditive ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Prelude.Nat.Nat -> Prelude.Nat.Additive
--- Prelude.Nat.GetMultiplicative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Prelude.Nat.Nat -> Prelude.Nat.Multiplicative
--- Language.Reflection.GoalType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} String -> Language.Reflection.Tactic -> Language.Reflection.Tactic
--- Language.Reflection.Guess ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 3, nt_unique = False} {a : Type ./Language/Reflection.idr.x141} -> a -> a -> Language.Reflection.Binder a
--- Language.Reflection.Hole ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection.idr.p141} -> a -> Language.Reflection.Binder a
--- Language.Reflection.I ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Int -> Language.Reflection.Const
--- IO' ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 19, nt_arity = 2} FFI -> Type ./IO.idr.d11 -> Type ./IO.idr.g11
--- Language.Reflection.IT16 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Language.Reflection.NativeTy
--- Language.Reflection.IT32 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Language.Reflection.NativeTy
--- Language.Reflection.IT64 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} Language.Reflection.NativeTy
--- Language.Reflection.IT8 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Language.Reflection.NativeTy
--- Language.Reflection.ITBig ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Language.Reflection.IntTy
--- Language.Reflection.ITChar ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} Language.Reflection.IntTy
--- Language.Reflection.ITFixed ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Language.Reflection.NativeTy -> Language.Reflection.IntTy
--- Language.Reflection.ITNative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Language.Reflection.IntTy
--- Language.Reflection.Implementation ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 8, nt_arity = 0, nt_unique = False} Language.Reflection.Tactic
--- Language.Reflection.ImplementationCtorN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 7, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.SpecialName
--- Language.Reflection.ImplementationN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Prelude.List.List String -> Language.Reflection.SpecialName
--- Language.Reflection.Elab.Implicit ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Plicity
--- Prelude.List.InBounds ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 22, nt_arity = 3} {a : Type ./Prelude/List.idr.z12} -> Prelude.Nat.Nat -> Prelude.List.List a -> Type ./Prelude/List.idr.e13
--- Prelude.List.InFirst ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} ({phTy1} : Type ./Prelude/List.idr.g13) -> {xs : Prelude.List.List {phTy1}} -> {x : {phTy1}} -> Prelude.List.InBounds {phTy1} Prelude.Nat.Z (Prelude.List.:: {phTy1} x xs)
--- Prelude.List.InLater ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 5, nt_unique = False} ({phTy1} : Type ./Prelude/List.idr.l13) -> {xs : Prelude.List.List {phTy1}} -> {x : {phTy1}} -> {k : Prelude.Nat.Nat} -> Prelude.List.InBounds {phTy1} k xs -> Prelude.List.InBounds {phTy1} (Prelude.Nat.S k) (Prelude.List.:: {phTy1} x xs)
--- Language.Reflection.Errors.Inaccessible ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 25, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.IncompleteTerm ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 21, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Language.Reflection.Induction ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 19, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Tactic
--- Infinite ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} DelayReason
--- Language.Reflection.Errors.InfiniteUnify ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 3, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TT -> Prelude.List.List (Builtins.Pair Language.Reflection.TTName Language.Reflection.TT) -> Language.Reflection.Errors.Err
--- Language.Reflection.Elab.Infix ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 1, nt_unique = False} Prelude.Nat.Nat -> Language.Reflection.Elab.Fixity
--- Language.Reflection.Elab.Infixl ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Prelude.Nat.Nat -> Language.Reflection.Elab.Fixity
--- Language.Reflection.Elab.Infixr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} Prelude.Nat.Nat -> Language.Reflection.Elab.Fixity
--- Language.Reflection.IntTy ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 272, nt_arity = 0} Type ./Language/Reflection.idr.z136
--- Prelude.Interfaces.Integral ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 305, nt_arity = 1} Type ./Prelude/Interfaces.idr.s128 -> Type ./Prelude/Interfaces.idr.v128
--- Language.Reflection.Errors.InternalMsg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} String -> Language.Reflection.Errors.Err
--- Language.Reflection.Intro ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 11, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Tactic
--- Language.Reflection.Intros ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 10, nt_arity = 0, nt_unique = False} Language.Reflection.Tactic
--- Language.Reflection.Errors.InvalidTCArg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 18, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Prelude.Maybe.IsJust ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 13, nt_arity = 2} {a : Type ./Prelude/Maybe.idr.y2} -> Prelude.Maybe.Maybe a -> Type ./Prelude/Maybe.idr.c3
--- Prelude.List.IsNonEmpty ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} ({phTy1} : Type ./Prelude/List.idr.d9) -> {xs : Prelude.List.List {phTy1}} -> {x : {phTy1}} -> Prelude.List.NonEmpty {phTy1} (Prelude.List.:: {phTy1} x xs)
--- Prelude.Maybe.ItIsJust ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} ({phTy0} : Type ./Prelude/Maybe.idr.e3) -> {x : {phTy0}} -> Prelude.Maybe.IsJust {phTy0} (Prelude.Maybe.Just {phTy0} x)
--- JS_Float ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} JS_Types Double
--- JS_Fn ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {t : Type ./IO.idr.u53} -> {s : Type ./IO.idr.x53} -> JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
--- JS_FnBase ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 2, nt_unique = False} {t : Type ./IO.idr.i54} -> JS_Types t -> JS_FnTypes t
--- JS_FnIO ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 3, nt_unique = False} {t : Type ./IO.idr.d54} -> {l : FFI} -> JS_Types t -> JS_FnTypes (IO' l t)
--- JS_FnT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not strictly positive
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 2, nt_unique = False} {a : Type ./IO.idr.x56} -> JS_FnTypes a -> JS_Types (JsFn a)
--- JS_FnTypes ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 63, nt_arity = 1} Type ./IO.idr.p53 -> Type ./IO.idr.s53
--- JS_IntChar ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} JS_IntTypes Char
--- JS_IntNative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} JS_IntTypes Int
--- JS_IntT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 2, nt_unique = False} {i : Type ./IO.idr.b57} -> JS_IntTypes i -> JS_Types i
--- JS_IntTypes ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 61, nt_arity = 1} Type ./IO.idr.e51 -> Type ./IO.idr.h51
--- JS_Ptr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} JS_Types Ptr
--- JS_Str ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} JS_Types String
--- JS_Types ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 65, nt_arity = 1} Type ./IO.idr.s56 -> Type ./IO.idr.v56
--- JS_Unit ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} JS_Types Unit
--- JsFn ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 60, nt_arity = 1} Type ./IO.idr.v50 -> Type ./IO.idr.y50
--- Prelude.Maybe.Just ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} {a : Type ./Prelude/Maybe.idr.c1} -> a -> Prelude.Maybe.Maybe a
--- Prelude.Interfaces.LT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Prelude.Interfaces.Ordering
--- Prelude.Nat.LTE ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 41, nt_arity = 2} Prelude.Nat.Nat -> Prelude.Nat.Nat -> Type ./Prelude/Nat.idr.w10
--- Prelude.Nat.LTESucc ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 3, nt_unique = False} {right : Prelude.Nat.Nat} -> {left : Prelude.Nat.Nat} -> Prelude.Nat.LTE left right -> Prelude.Nat.LTE (Prelude.Nat.S left) (Prelude.Nat.S right)
--- Prelude.Nat.LTEZero ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} {right : Prelude.Nat.Nat} -> Prelude.Nat.LTE Prelude.Nat.Z right
--- Language.Reflection.Lam ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection.idr.b141} -> a -> Language.Reflection.Binder a
--- LazyValue ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} DelayReason
--- Prelude.Either.Left ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {b : Type ./Prelude/Either.idr.c1} -> {a : Type ./Prelude/Either.idr.f1} -> a -> Prelude.Either.Either a b
--- Prelude.Nat.LeftIsNotZero ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {m : Prelude.Nat.Nat} -> {n : Prelude.Nat.Nat} -> Prelude.Nat.NotBothZero (Prelude.Nat.S n) m
--- Language.Reflection.Let ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 3, nt_unique = False} {a : Type ./Language/Reflection.idr.k141} -> a -> a -> Language.Reflection.Binder a
--- Language.Reflection.LetTac ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 21, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TT -> Language.Reflection.Tactic
--- Language.Reflection.LetTacTy ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 22, nt_arity = 3, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.Tactic
--- Prelude.List.List ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} Type ./Prelude/List.idr.u -> Type ./Prelude/List.idr.x
--- Language.Reflection.Errors.LoadingFailed ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 32, nt_arity = 2, nt_unique = False} String -> Language.Reflection.Errors.Err -> Language.Reflection.Errors.Err
--- Language.Reflection.MN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 2, nt_unique = False} Int -> String -> Language.Reflection.TTName
--- ManagedPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 0, nt_arity = 0} Type ./Builtins.idr.b29
--- Prelude.Interfaces.MaxBound ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 273, nt_arity = 1} Type ./Prelude/Interfaces.idr.p121 -> Type ./Prelude/Interfaces.idr.s121
--- Prelude.Maybe.Maybe ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} Type ./Prelude/Maybe.idr.u -> Type ./Prelude/Maybe.idr.x
--- Language.Reflection.MetaN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 8, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TTName -> Language.Reflection.SpecialName
--- Language.Reflection.MethodN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.SpecialName
--- Prelude.Interfaces.MinBound ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 270, nt_arity = 1} Type ./Prelude/Interfaces.idr.v119 -> Type ./Prelude/Interfaces.idr.y119
--- FFI_C.MkCFnPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {t : Type ./IO.idr.v38} -> t -> FFI_C.CFnPtr t
--- Builtins.MkDPair ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {a : Type ./Builtins.idr.f8} -> {P : a -> Type ./Builtins.idr.j8} -> (x : a) -> P x -> Builtins.DPair a P
--- Language.Reflection.Elab.MkDatatype ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} Language.Reflection.TTName -> Prelude.List.List Language.Reflection.Elab.TyConArg -> Language.Reflection.Raw -> Prelude.List.List (Builtins.Pair Language.Reflection.TTName (Builtins.Pair (Prelude.List.List Language.Reflection.Elab.CtorArg) Language.Reflection.Raw)) -> Language.Reflection.Elab.Datatype
--- MkFFI ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} (Type ./IO.idr.c2 -> Type ./IO.idr.f2) -> Type ./IO.idr.i2 -> Type ./IO.idr.l2 -> FFI
--- Language.Reflection.Elab.MkFunArg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Raw -> Language.Reflection.Elab.Plicity -> Language.Reflection.Elab.Erasure -> Language.Reflection.Elab.FunArg
--- Language.Reflection.Elab.MkFunClause ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {a : Type ./Language/Reflection/Elab.idr.y7} -> a -> a -> Language.Reflection.Elab.FunClause a
--- MkIO ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {a : Type ./IO.idr.i11} -> {lang : FFI} -> (World -> PrimIO (WorldRes a)) -> IO' lang a
--- Language.Reflection.Elab.MkImpossibleClause ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection/Elab.idr.d8} -> a -> Language.Reflection.Elab.FunClause a
--- MkJsFn ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {t : Type ./IO.idr.a51} -> t -> JsFn t
--- Builtins.MkPair ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {A : Type ./Builtins.idr.w2} -> {B : Type ./Builtins.idr.z2} -> A -> B -> Builtins.Pair A B
--- FFI_C.MkRaw ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {t : Type ./IO.idr.m38} -> t -> FFI_C.Raw t
--- Builtins.MkUPair ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {A : AnyType} -> {B : AnyType} -> A -> B -> Builtins.UPair A B
--- MkUnit ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Unit
--- Prelude.File.Mode ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 28, nt_arity = 0} Type ./Prelude/File.idr.n4
--- Prelude.Monad.Monad ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} (Type ./Prelude/Monad.idr.u -> Type ./Prelude/Monad.idr.x) -> Type ./Prelude/Monad.idr.a1
--- Prelude.Algebra.Monoid ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 10, nt_arity = 1} Type ./Prelude/Algebra.idr.d2 -> Type ./Prelude/Algebra.idr.g2
--- Language.Reflection.Errors.Msg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} String -> Language.Reflection.Errors.Err
--- Prelude.Nat.Multiplicative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 111, nt_arity = 0} Type ./Prelude/Nat.idr.k28
--- Language.Reflection.NS ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Prelude.List.List String -> Language.Reflection.TTName
--- Language.Reflection.NamePart ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.ErrorReportPart
--- Language.Reflection.NameType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 296, nt_arity = 0} Type ./Language/Reflection.idr.q140
--- Prelude.Nat.Nat ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 0} Type ./Prelude/Nat.idr.u
--- Language.Reflection.NativeTy ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 271, nt_arity = 0} Type ./Language/Reflection.idr.x136
--- Prelude.Interfaces.Neg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 204, nt_arity = 1} Type ./Prelude/Interfaces.idr.l100 -> Type ./Prelude/Interfaces.idr.o100
--- ForeignEnv.Nil ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} {f : FFI} -> ForeignEnv.FEnv f (Prelude.List.Nil Type ./IO.idr.g16)
--- Prelude.List.Nil ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} {elem : Type ./Prelude/List.idr.z} -> Prelude.List.List elem
--- Prelude.Basics.No ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} {prop : Type ./Prelude/Basics.idr.q13} -> (prop -> Void) -> Prelude.Basics.Dec prop
--- Language.Reflection.Errors.NoEliminator ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 22, nt_arity = 2, nt_unique = False} String -> Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.NoRewriting ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 30, nt_arity = 3, nt_unique = False} Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.NoSuchVariable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 12, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.NoTypeDecl ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 15, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.NoValidAlts ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 20, nt_arity = 1, nt_unique = False} Prelude.List.List Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Language.Reflection.Errors.NonCollapsiblePostulate ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 27, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Prelude.List.NonEmpty ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 17, nt_arity = 2} {a : Type ./Prelude/List.idr.x8} -> Prelude.List.List a -> Type ./Prelude/List.idr.b9
--- Language.Reflection.Errors.NonFunctionType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 8, nt_arity = 2, nt_unique = False} Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Prelude.Nat.NotBothZero ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 39, nt_arity = 2} Prelude.Nat.Nat -> Prelude.Nat.Nat -> Type ./Prelude/Nat.idr.s8
--- Language.Reflection.Errors.NotEquality ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 9, nt_arity = 2, nt_unique = False} Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Language.Reflection.Elab.NotErased ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Erasure
--- Language.Reflection.Errors.NotInjective ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 16, nt_arity = 3, nt_unique = False} Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Prelude.Maybe.Nothing ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} {a : Type ./Prelude/Maybe.idr.z} -> Prelude.Maybe.Maybe a
--- Language.Reflection.NullType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Language.Reflection.Universe
--- Prelude.Interfaces.Num ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 172, nt_arity = 1} Type ./Prelude/Interfaces.idr.y91 -> Type ./Prelude/Interfaces.idr.b92
--- Prelude.Show.Open ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Prelude.Show.Prec
--- Prelude.Interfaces.Ord ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 65, nt_arity = 1} Type ./Prelude/Interfaces.idr.s22 -> Type ./Prelude/Interfaces.idr.v22
--- Prelude.Interfaces.Ordering ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 49, nt_arity = 0} Type ./Prelude/Interfaces.idr.a17
--- Language.Reflection.P ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} Language.Reflection.NameType -> Language.Reflection.TTName -> Language.Reflection.TT -> Language.Reflection.TT
--- Language.Reflection.PVTy ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 7, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection.idr.g142} -> a -> Language.Reflection.Binder a
--- Language.Reflection.PVar ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection.idr.c142} -> a -> Language.Reflection.Binder a
--- Builtins.Pair ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 11, nt_arity = 2} Type ./Builtins.idr.o2 -> Type ./Builtins.idr.r2 -> Type ./Builtins.idr.u2
--- Language.Reflection.ParentN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> String -> Language.Reflection.SpecialName
--- Prelude.File.PermissionDenied ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 0, nt_unique = False} Prelude.File.FileError
--- Language.Reflection.Pi ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 3, nt_unique = False} {a : Type ./Language/Reflection.idr.f141} -> a -> a -> Language.Reflection.Binder a
--- Language.Reflection.Elab.Plicity ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 10, nt_arity = 0} Type ./Language/Reflection/Elab.idr.c1
--- Prelude.Show.Prec ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 0} Type ./Prelude/Show.idr.u
--- Language.Reflection.Elab.Prefix ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 1, nt_unique = False} Prelude.Nat.Nat -> Language.Reflection.Elab.Fixity
--- Prelude.Show.PrefixMinus ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 0, nt_unique = False} Prelude.Show.Prec
--- PrimIO ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} Type ./IO.idr.u -> Type ./IO.idr.x
--- Language.Reflection.Elab.Prim__AddImplementation ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 38, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Apply ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 18, nt_arity = 2, nt_unique = False} Language.Reflection.Raw -> Prelude.List.List Prelude.Bool.Bool -> Language.Reflection.Elab.Elab (Prelude.List.List (Builtins.Pair Language.Reflection.TTName Language.Reflection.TTName))
--- Language.Reflection.Elab.Prim__Attack ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 22, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__BindElab ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 4, nt_unique = False} {a : Type ./Language/Reflection/Elab.idr.x20} -> {b : Type ./Language/Reflection/Elab.idr.a21} -> Language.Reflection.Elab.Elab a -> (a -> Language.Reflection.Elab.Elab b) -> Language.Reflection.Elab.Elab b
--- Language.Reflection.Elab.Prim__Check ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 12, nt_arity = 2, nt_unique = False} Prelude.List.List (Builtins.Pair Language.Reflection.TTName (Language.Reflection.Binder Language.Reflection.TT)) -> Language.Reflection.Raw -> Language.Reflection.Elab.Elab (Builtins.Pair Language.Reflection.TT Language.Reflection.TT)
--- Language.Reflection.Elab.Prim__Claim ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 24, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Raw -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Compute ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 30, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Converts ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 33, nt_arity = 3, nt_unique = False} Prelude.List.List (Builtins.Pair Language.Reflection.TTName (Language.Reflection.Binder Language.Reflection.TT)) -> Language.Reflection.TT -> Language.Reflection.TT -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Debug ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 44, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection/Elab.idr.h23} -> Prelude.List.List Language.Reflection.ErrorReportPart -> Language.Reflection.Elab.Elab a
--- Language.Reflection.Elab.Prim__DeclareDatatype ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 36, nt_arity = 1, nt_unique = False} Language.Reflection.Elab.TyDecl -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__DeclareType ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 34, nt_arity = 1, nt_unique = False} Language.Reflection.Elab.TyDecl -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__DefineDatatype ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 37, nt_arity = 1, nt_unique = False} Language.Reflection.Elab.DataDefn -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__DefineFunction ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 35, nt_arity = 1, nt_unique = False} Language.Reflection.Elab.FunDefn Language.Reflection.Raw -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Env ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab (Prelude.List.List (Builtins.Pair Language.Reflection.TTName (Language.Reflection.Binder Language.Reflection.TT)))
--- Language.Reflection.Elab.Prim__Fail ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection/Elab.idr.l21} -> Prelude.List.List Language.Reflection.ErrorReportPart -> Language.Reflection.Elab.Elab a
--- Language.Reflection.Elab.Prim__Fill ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 17, nt_arity = 1, nt_unique = False} Language.Reflection.Raw -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Fixity ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 43, nt_arity = 1, nt_unique = False} String -> Language.Reflection.Elab.Elab Language.Reflection.Elab.Fixity
--- Language.Reflection.Elab.Prim__Focus ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 20, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Forall ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 26, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Raw -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Gensym ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 15, nt_arity = 1, nt_unique = False} String -> Language.Reflection.Elab.Elab Language.Reflection.TTName
--- Language.Reflection.Elab.Prim__Goal ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab (Builtins.Pair Language.Reflection.TTName Language.Reflection.TT)
--- Language.Reflection.Elab.Prim__Guess ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 7, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab Language.Reflection.TT
--- Language.Reflection.Elab.Prim__Holes ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab (Prelude.List.List Language.Reflection.TTName)
--- Prim__IO ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {a : Type ./IO.idr.z} -> a -> PrimIO a
--- Language.Reflection.Elab.Prim__Intro ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 25, nt_arity = 1, nt_unique = False} Prelude.Maybe.Maybe Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__IsTCName ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 39, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab Prelude.Bool.Bool
--- Language.Reflection.Elab.Prim__LetBind ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 29, nt_arity = 3, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Raw -> Language.Reflection.Raw -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__LookupArgs ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 11, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab (Prelude.List.List (Builtins.Pair Language.Reflection.TTName (Builtins.Pair (Prelude.List.List Language.Reflection.Elab.FunArg) Language.Reflection.Raw)))
--- Language.Reflection.Elab.Prim__LookupDatatype ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 9, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab (Prelude.List.List Language.Reflection.Elab.Datatype)
--- Language.Reflection.Elab.Prim__LookupFunDefn ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 10, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab (Prelude.List.List (Language.Reflection.Elab.FunDefn Language.Reflection.TT))
--- Language.Reflection.Elab.Prim__LookupTy ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 8, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab (Prelude.List.List (Builtins.Pair Language.Reflection.TTName (Builtins.Pair Language.Reflection.NameType Language.Reflection.TT)))
--- Language.Reflection.Elab.Prim__MatchApply ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 19, nt_arity = 2, nt_unique = False} Language.Reflection.Raw -> Prelude.List.List Prelude.Bool.Bool -> Language.Reflection.Elab.Elab (Prelude.List.List (Builtins.Pair Language.Reflection.TTName Language.Reflection.TTName))
--- Language.Reflection.Elab.Prim__Metavar ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 45, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Namespace ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 14, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab (Prelude.List.List String)
--- Language.Reflection.Elab.Prim__Normalise ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 31, nt_arity = 2, nt_unique = False} Prelude.List.List (Builtins.Pair Language.Reflection.TTName (Language.Reflection.Binder Language.Reflection.TT)) -> Language.Reflection.TT -> Language.Reflection.Elab.Elab Language.Reflection.TT
--- Language.Reflection.Elab.Prim__PatBind ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 28, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__PatVar ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 27, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__PureElab ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection/Elab.idr.t20} -> a -> Language.Reflection.Elab.Elab a
--- Language.Reflection.Elab.Prim__RecursiveElab ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 42, nt_arity = 2, nt_unique = False} Language.Reflection.Raw -> Language.Reflection.Elab.Elab Unit -> Language.Reflection.Elab.Elab (Builtins.Pair Language.Reflection.TT Language.Reflection.TT)
--- Language.Reflection.Elab.Prim__ResolveTC ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 40, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Rewrite ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 23, nt_arity = 1, nt_unique = False} Language.Reflection.Raw -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Search ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 41, nt_arity = 2, nt_unique = False} Int -> Prelude.List.List Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Solve ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 16, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__SourceLocation ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 13, nt_arity = 0, nt_unique = False} Language.Reflection.Elab.Elab Language.Reflection.SourceLocation
--- Language.Reflection.Elab.Prim__Try ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 3, nt_unique = False} {a : Type ./Language/Reflection/Elab.idr.g21} -> Language.Reflection.Elab.Elab a -> Language.Reflection.Elab.Elab a -> Language.Reflection.Elab.Elab a
--- Language.Reflection.Elab.Prim__Unfocus ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 21, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Elab.Elab Unit
--- Language.Reflection.Elab.Prim__Whnf ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 32, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Elab.Elab Language.Reflection.TT
--- Language.Reflection.Errors.ProgramLineComment ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 24, nt_arity = 0, nt_unique = False} Language.Reflection.Errors.Err
--- Language.Reflection.Errors.ProofSearchFail ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 29, nt_arity = 1, nt_unique = False} Language.Reflection.Errors.Err -> Language.Reflection.Errors.Err
--- Prelude.Providers.Provide ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {a : Type ./Prelude/Providers.idr.z} -> a -> Prelude.Providers.Provider a
--- Prelude.Providers.Provider ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} Type ./Prelude/Providers.idr.u -> Type ./Prelude/Providers.idr.x
--- Language.Reflection.Errors.ProviderError ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 31, nt_arity = 1, nt_unique = False} String -> Language.Reflection.Errors.Err
--- Ptr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 0, nt_arity = 0} Type ./Builtins.idr.z28
--- Language.Reflection.Quotable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 331, nt_arity = 2} Type ./Language/Reflection.idr.s174 -> Type ./Language/Reflection.idr.v174 -> Type ./Language/Reflection.idr.y174
--- Language.Reflection.RApp ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 2, nt_unique = False} Language.Reflection.Raw -> Language.Reflection.Raw -> Language.Reflection.Raw
--- Language.Reflection.RBind ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 3, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Binder Language.Reflection.Raw -> Language.Reflection.Raw -> Language.Reflection.Raw
--- Language.Reflection.RConstant ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 1, nt_unique = False} Language.Reflection.Const -> Language.Reflection.Raw
--- Language.Reflection.RType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} Language.Reflection.Raw
--- Language.Reflection.RUType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 1, nt_unique = False} Language.Reflection.Universe -> Language.Reflection.Raw
--- FFI_C.Raw ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 44, nt_arity = 1} Type ./IO.idr.h38 -> Type ./IO.idr.k38
--- Language.Reflection.Raw ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 328, nt_arity = 0} Type ./Language/Reflection.idr.z172
--- Language.Reflection.RawPart ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 1, nt_unique = False} Language.Reflection.Raw -> Language.Reflection.ErrorReportPart
--- Prelude.File.Read ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Prelude.File.Mode
--- Ownership.Read ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {a : UniqueType} -> a -> Ownership.Borrowed a
--- Prelude.File.ReadAppend ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 0, nt_unique = False} Prelude.File.Mode
--- Prelude.File.ReadWrite ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 0, nt_unique = False} Prelude.File.Mode
--- Prelude.File.ReadWriteTruncate ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 0, nt_unique = False} Prelude.File.Mode
--- Language.Reflection.Ref ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Language.Reflection.NameType
--- Language.Reflection.Refine ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Tactic
--- Refl ---
RigCount: RigW
Injectivity: True
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {A : Type primitive.q} -> {x : A} -> = A A x x
--- Language.Reflection.ReflConst ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 275, nt_arity = 1} Type ./Language/Reflection.idr.r137 -> Type ./Language/Reflection.idr.u137
--- Language.Reflection.Reflect ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 13, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Tactic
--- Language.Reflection.Rewrite ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 18, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Tactic
--- Prelude.Either.Right ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 3, nt_unique = False} {b : Type ./Prelude/Either.idr.j1} -> {a : Type ./Prelude/Either.idr.m1} -> b -> Prelude.Either.Either a b
--- Prelude.Nat.RightIsNotZero ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} {m : Prelude.Nat.Nat} -> {n : Prelude.Nat.Nat} -> Prelude.Nat.NotBothZero n (Prelude.Nat.S m)
--- Prelude.Nat.S ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} Prelude.Nat.Nat -> Prelude.Nat.Nat
--- Language.Reflection.SN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 1, nt_unique = False} Language.Reflection.SpecialName -> Language.Reflection.TTName
--- Language.Reflection.Search ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 7, nt_arity = 1, nt_unique = False} Int -> Language.Reflection.Tactic
--- Prelude.Algebra.Semigroup ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} Type ./Prelude/Algebra.idr.u -> Type ./Prelude/Algebra.idr.x
--- Language.Reflection.Seq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 2, nt_unique = False} Language.Reflection.Tactic -> Language.Reflection.Tactic -> Language.Reflection.Tactic
--- Prelude.Show.Show ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 34, nt_arity = 1} Type ./Prelude/Show.idr.d6 -> Type ./Prelude/Show.idr.g6
--- Language.Reflection.Skip ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 24, nt_arity = 0, nt_unique = False} Language.Reflection.Tactic
--- Language.Reflection.Solve ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 9, nt_arity = 0, nt_unique = False} Language.Reflection.Tactic
--- Language.Reflection.SourceFC ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 26, nt_arity = 0, nt_unique = False} Language.Reflection.Tactic
--- Language.Reflection.SourceLocation ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 0} Type ./Language/Reflection.idr.u
--- Language.Reflection.SpecialName ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 33, nt_arity = 0} Type ./Language/Reflection.idr.s9
--- Language.Reflection.Str ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 1, nt_unique = False} String -> Language.Reflection.Const
--- Prelude.Strings.StrCons ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} (x : Char) -> (xs : String) -> Prelude.Strings.StrM (Prelude.Strings.strCons x xs)
--- Prelude.Strings.StrM ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 22, nt_arity = 1} String -> Type ./Prelude/Strings.idr.v4
--- Prelude.Strings.StrNil ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Prelude.Strings.StrM ""
--- Language.Reflection.StrType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 10, nt_arity = 0, nt_unique = False} Language.Reflection.Const
--- Prelude.Stream.Stream ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} Type ./Prelude/Stream.idr.u -> Type ./Prelude/Stream.idr.x
--- Language.Reflection.SubReport ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 1, nt_unique = False} Prelude.List.List Language.Reflection.ErrorReportPart -> Language.Reflection.ErrorReportPart
--- Prelude.Pairs.Subset ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 10, nt_arity = 2} (a : Type ./Prelude/Pairs.idr.q2) -> (a -> Type ./Prelude/Pairs.idr.u2) -> Type ./Prelude/Pairs.idr.x2
--- Symbol_ ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 19, nt_arity = 1} String -> Type ./Builtins.idr.j12
--- Language.Reflection.TCon ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 3, nt_arity = 2, nt_unique = False} Int -> Int -> Language.Reflection.NameType
--- Language.Reflection.TConst ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 1, nt_unique = False} Language.Reflection.Const -> Language.Reflection.TT
--- Language.Reflection.TT ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 327, nt_arity = 0} Type ./Language/Reflection.idr.l172
--- Language.Reflection.TTName ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 32, nt_arity = 0} Type ./Language/Reflection.idr.k9
--- Language.Reflection.TTUExp ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 270, nt_arity = 0} Type ./Language/Reflection.idr.s136
--- Language.Reflection.TType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 1, nt_unique = False} Language.Reflection.TTUExp -> Language.Reflection.TT
--- Language.Reflection.Tactic ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 330, nt_arity = 0} Type ./Language/Reflection.idr.q173
--- Language.Reflection.TermPart ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 2, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.ErrorReportPart
--- Language.Reflection.TextPart ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} String -> Language.Reflection.ErrorReportPart
--- TheWorld ---
RigCount: RigW
Injectivity: False
Accessibility: private
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} prim__WorldType -> World
--- Language.Reflection.TheWorld ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 14, nt_arity = 0, nt_unique = False} Language.Reflection.Const
--- Language.Reflection.Errors.TooManyArguments ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 10, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Prelude.Traversable.Traversable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 11, nt_arity = 1} (Type ./Prelude/Traversable.idr.i10 -> Type ./Prelude/Traversable.idr.l10) -> Type ./Prelude/Traversable.idr.o10
--- Language.Reflection.Trivial ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 0, nt_unique = False} Language.Reflection.Tactic
--- Prelude.Bool.True ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Prelude.Bool.Bool
--- Language.Reflection.Try ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} Language.Reflection.Tactic -> Language.Reflection.Tactic -> Language.Reflection.Tactic
--- Language.Reflection.Elab.TyConArg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 20, nt_arity = 0} Type ./Language/Reflection/Elab.idr.c5
--- Language.Reflection.Elab.TyConIndex ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} Language.Reflection.Elab.FunArg -> Language.Reflection.Elab.TyConArg
--- Language.Reflection.Elab.TyConParameter ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Language.Reflection.Elab.FunArg -> Language.Reflection.Elab.TyConArg
--- Language.Reflection.Elab.TyDecl ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 21, nt_arity = 0} Type ./Language/Reflection/Elab.idr.g5
--- Language.Reflection.UN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} String -> Language.Reflection.TTName
--- Builtins.UPair ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 14, nt_arity = 2} AnyType -> AnyType -> AnyType
--- Language.Reflection.UType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 7, nt_arity = 1, nt_unique = False} Language.Reflection.Universe -> Language.Reflection.TT
--- Language.Reflection.UVal ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} Int -> Language.Reflection.TTUExp
--- Language.Reflection.UVar ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} String -> Int -> Language.Reflection.TTUExp
--- Language.Reflection.Unfocus ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 5, nt_arity = 0, nt_unique = False} Language.Reflection.Tactic
--- Language.Reflection.Errors.UnifyScope ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 6, nt_arity = 4, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TTName -> Language.Reflection.TT -> Prelude.List.List (Builtins.Pair Language.Reflection.TTName Language.Reflection.TT) -> Language.Reflection.Errors.Err
--- Prelude.Uninhabited.Uninhabited ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 1} Type ./Prelude/Uninhabited.idr.u -> Type ./Prelude/Uninhabited.idr.x
--- Language.Reflection.UniqueType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Language.Reflection.Universe
--- Unit ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 8, nt_arity = 0} Type ./Builtins.idr.u
--- Language.Reflection.Universe ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 326, nt_arity = 0} Type ./Language/Reflection.idr.j172
--- Language.Reflection.Errors.UniverseError ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 23, nt_arity = 0, nt_unique = False} Language.Reflection.Errors.Err
--- Language.Reflection.Errors.UnknownImplicit ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 26, nt_arity = 2, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.TTName -> Language.Reflection.Errors.Err
--- Prelude.Show.User ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 4, nt_arity = 1, nt_unique = False} Prelude.Nat.Nat -> Prelude.Show.Prec
--- Language.Reflection.V ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 1, nt_unique = False} Int -> Language.Reflection.TT
--- Language.Reflection.Var ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 1, nt_unique = False} Language.Reflection.TTName -> Language.Reflection.Raw
--- Void ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 18, nt_arity = 0} Type ./Builtins.idr.e11
--- Language.Reflection.VoidType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 11, nt_arity = 0, nt_unique = False} Language.Reflection.Const
--- Prelude.WellFounded.WellFounded ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 10, nt_arity = 2} {a : Type ./Prelude/WellFounded.idr.j4} -> (a -> a -> Type ./Prelude/WellFounded.idr.o4) -> Type ./Prelude/WellFounded.idr.r4
--- Language.Reflection.WhereN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} Int -> Language.Reflection.TTName -> Language.Reflection.TTName -> Language.Reflection.SpecialName
--- Language.Reflection.Errors.WithFnType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 13, nt_arity = 1, nt_unique = False} Language.Reflection.TT -> Language.Reflection.Errors.Err
--- Language.Reflection.WithN ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} Int -> Language.Reflection.TTName -> Language.Reflection.SpecialName
--- World ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: TCon {nt_tag = 9, nt_arity = 0} Type ./IO.idr.d1
--- Language.Reflection.WorldType ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 13, nt_arity = 0, nt_unique = False} Language.Reflection.Const
--- Prelude.File.WriteTruncate ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 1, nt_arity = 0, nt_unique = False} Prelude.File.Mode
--- Prelude.Basics.Yes ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {prop : Type ./Prelude/Basics.idr.m13} -> prop -> Prelude.Basics.Dec prop
--- Prelude.Nat.Z ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 0, nt_unique = False} Prelude.Nat.Nat
--- assert_unreachable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref {a : Type ./Builtins.idr.g26} -> a
--- call__IO ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: Total
MetaInformation: EmptyMI
---
Case: {a : Type ./IO.idr.b35} -> {ffi : FFI} -> IO' ffi a -> PrimIO a []
COMPILE TIME:
[{e0},{e1},{e2}] case {e2} of
MkIO({i3}, {i4}, {e5}) => {e5} (TheWorld prim__TheWorld)
RUN TIME:
[{e0},{e1},{e2}] case {e2} of
MkIO({i3}, {i4}, {e5}) => {e5} (TheWorld prim__TheWorld)
Inlinable
--- idris_crash ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref {a : Type ./Builtins.idr.n26} -> String -> a
--- io_bind ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: Total
MetaInformation: EmptyMI
---
Case: {b : Type ./IO.idr.g30} -> {l : FFI} -> {a : Type ./IO.idr.k30} -> IO' l a -> (a -> IO' l b) -> IO' l b []
COMPILE TIME:
[{e0},{e1},{e2},{e3},{e4}] case {e3} of
MkIO({i5}, {i6}, {e7}) => MkIO {e0} {e1} (\ w : World => prim_io_bind (WorldRes {e0}) (WorldRes {e2}) ({e7} w) (\ {b0} : WorldRes {e2} => let {scvar126} : IO' {e1} {e0} = {e4} {b0} in case block in io_bind at IO.idr:107:34 {e0} {e1} {e2} {e7} {e4} w {b0} {scvar126}))
RUN TIME:
[{e0},{e1},{e2},{e3},{e4}] case {e3} of
MkIO({i5}, {i6}, {e7}) => MkIO {e0} {e1} (\ w : [__] => prim_io_bind {e0} {e2} ({e7} w) (\ {b0} : [__] => case block in io_bind at IO.idr:107:34 {e0} {e1} {e2} {e7} {e4} w {b0} ({e4} {b0})))
Not inlinable
--- io_pure ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: Total
MetaInformation: EmptyMI
---
Case: {a : Type ./IO.idr.m33} -> {l : FFI} -> a -> IO' l a []
COMPILE TIME:
[{e0},{e1},{e2}] MkIO {e0} {e1} (\ w : World => prim_io_pure (WorldRes {e0}) {e2})
RUN TIME:
[{e0},{e1},{e2}] MkIO {e0} {e1} (\ w : [__] => Prim__IO {e0} {e2})
Inlinable
--- Main.main ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
Case: IO Unit []
COMPILE TIME:
[] Prelude.Interactive.putStrLn "Hello, Idris!"
RUN TIME:
[] Prelude.Interactive.putStr' (MkFFI FFI_C.C_Types String String) "Hello, Idris!\n"
Inlinable
--- mkForeignPrim ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref {xs : Prelude.List.List Type ./IO.idr.o23} -> {ffi : FFI} -> {env : ForeignEnv.FEnv ffi xs} -> {t : Type ./IO.idr.s23} -> ForeignPrimType ffi xs env t
--- prim__asPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref ManagedPtr -> Ptr
--- prim__eqManagedPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref ManagedPtr -> ManagedPtr -> Int
--- prim__eqPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref Ptr -> Ptr -> Int
--- prim__null ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref Ptr
--- prim__peek16 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Bits16
--- prim__peek32 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Bits32
--- prim__peek64 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Bits64
--- prim__peek8 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Bits8
--- prim__peekDouble ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Double
--- prim__peekPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Ptr
--- prim__peekSingle ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Double
--- prim__poke16 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Bits16 -> Int
--- prim__poke32 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Bits32 -> Int
--- prim__poke64 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Bits64 -> Int
--- prim__poke8 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Bits8 -> Int
--- prim__pokeDouble ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Double -> Int
--- prim__pokePtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Ptr -> Int
--- prim__pokeSingle ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> Int -> Double -> Int
--- prim__ptrOffset ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref Ptr -> Int -> Ptr
--- prim__readFile ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> String
--- prim__registerPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref Ptr -> Int -> ManagedPtr
--- prim__sizeofPtr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref Int
--- prim__stderr ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref Ptr
--- prim__stdin ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref Ptr
--- prim__stdout ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref Ptr
--- prim__vm ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr
--- prim__writeFile ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref prim__WorldType -> Ptr -> String -> Int
--- prim__writeString ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
Operator: prim__WorldType -> String -> Int
--- prim_io_bind ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: Total
MetaInformation: EmptyMI
---
Case: {b : Type ./IO.idr.x27} -> {a : Type ./IO.idr.a28} -> PrimIO a -> (a -> PrimIO b) -> PrimIO b []
COMPILE TIME:
[{e0},{e1},{e2},{e3}] case {e2} of
Prim__IO({i4}, {e5}) => {e3} {e5}
RUN TIME:
[{e0},{e1},{e2},{e3}] case {e2} of
Prim__IO({i4}, {e5}) => {e3} {e5}
Inlinable
--- prim_write ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: Total
MetaInformation: EmptyMI
---
Case: {l : FFI} -> String -> IO' l Int []
COMPILE TIME:
[{e0},{e1}] MkIO Int {e0} (\ w : World => prim_io_pure (WorldRes Int) (prim__writeString (world w) {e1}))
RUN TIME:
[{e0},{e1}] MkIO Int {e0} (\ w : [__] => Prim__IO Int (prim__writeString (world w) {e1}))
Not inlinable
--- Prelude.Interactive.putStr' ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
Case: {ffi : FFI} -> String -> IO' ffi Unit []
COMPILE TIME:
[{e0},{e1}] Prelude.Monad.>>= (IO' {e0}) (Prelude.Monad.IO' ffi implementation of Prelude.Monad.Monad {e0}) Int Unit (prim_write {e0} {e1}) (\ {__bindx0} : Int => Prelude.Applicative.pure (IO' {e0}) (Prelude.Monad.IO' ffi implementation of Prelude.Applicative.Applicative {e0}) Unit MkUnit)
RUN TIME:
[{e0},{e1}] io_bind Unit {e0} Int (prim_write {e0} {e1}) (\ {__bindx0} : [__] => io_pure Unit {e0} MkUnit)
Not inlinable
--- run__IO ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: Total
MetaInformation: EmptyMI
---
Case: {ffi : FFI} -> IO' ffi Unit -> PrimIO Unit []
COMPILE TIME:
[{e0},{e1}] call__IO Unit {e0} {e1}
RUN TIME:
[{e0},{e1}] call__IO Unit {e0} {e1}
Inlinable
--- unsafePerformPrimIO ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref {a : Type ./IO.idr.c29} -> PrimIO a -> a
--- world ---
RigCount: RigW
Injectivity: False
Accessibility: export
Totality: Total
MetaInformation: EmptyMI
---
Case: World -> prim__WorldType []
COMPILE TIME:
[{e0}] case {e0} of
TheWorld({e1}) => {e1}
RUN TIME:
[{e0}] case {e0} of
TheWorld({e1}) => {e1}
Inlinable
--- {__Infer0} ---
RigCount: RigW
Injectivity: True
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: DataMI []
---
TyDecl: TCon {nt_tag = 6, nt_arity = 0} Type primitive.a
--- {__infer0} ---
RigCount: RigW
Injectivity: True
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {{iType0} : Type primitive.c} -> {iType0} -> {__Infer0}
--- Decidable.Equality.Decidable.Equality.Char implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref (x : Char) -> (y : Char) -> = Char Char x y -> Void
--- Decidable.Equality.Decidable.Equality.Int implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref (x : Int) -> (y : Int) -> = Int Int x y -> Void
--- Decidable.Equality.Decidable.Equality.Integer implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref (x : Integer) -> (y : Integer) -> = Integer Integer x y -> Void
--- Decidable.Equality.Decidable.Equality.ManagedPtr implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref (x : ManagedPtr) -> (y : ManagedPtr) -> = ManagedPtr ManagedPtr x y -> Void
--- Decidable.Equality.Decidable.Equality.Ptr implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref (x : Ptr) -> (y : Ptr) -> = Ptr Ptr x y -> Void
--- Decidable.Equality.Decidable.Equality.String implementation of Decidable.Equality.DecEq, method decEq, primitiveNotEq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref (x : String) -> (y : String) -> = String String x y -> Void
--- case block in io_bind at IO.idr:107:34 ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
Case: (b : Type ./IO.idr.b31) -> (l : FFI) -> (a : Type ./IO.idr.f31) -> (World -> PrimIO (WorldRes a)) -> (a -> IO' l b) -> World -> WorldRes a -> IO' l b -> PrimIO (WorldRes b) []
COMPILE TIME:
[{e0},{e1},{e2},{e3},{e4},{e5},{e6},{e7}] case {e7} of
MkIO({i8}, {i9}, {e10}) => {e10} {e5}
RUN TIME:
[{e0},{e1},{e2},{e3},{e4},{e5},{e6},{e7}] case {e7} of
MkIO({i8}, {i9}, {e10}) => {e10} {e5}
Inlinable
--- case block in Void at (casefun Void) ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref (prop : Void -> Type ./Builtins.idr.w11) -> (scrutinee : Void) -> prop scrutinee
--- <<Void eliminator>> ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: not yet checked for totality
MetaInformation: EmptyMI
---
TyDecl: Ref (prop : Void -> Type ./Builtins.idr.m11) -> (scrutinee : Void) -> prop scrutinee
--- constructor of Prelude.Applicative.Alternative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {f : Type ./Prelude/Applicative.idr.g25 -> Type ./Prelude/Applicative.idr.j25} -> Prelude.Applicative.Applicative f -> ((a : Type ./Prelude/Applicative.idr.n25) -> f a) -> ((a6 : Type ./Prelude/Applicative.idr.r25) -> f a6 -> f a6 -> f a6) -> Prelude.Applicative.Alternative f
--- constructor of Prelude.Applicative.Applicative ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {f : Type ./Prelude/Applicative.idr.c1 -> Type ./Prelude/Applicative.idr.f1} -> Prelude.Functor.Functor f -> ((a : Type ./Prelude/Applicative.idr.j1) -> a -> f a) -> ((b : Type ./Prelude/Applicative.idr.o1) -> (a8 : Type ./Prelude/Applicative.idr.r1) -> f (a8 -> b) -> f a8 -> f b) -> Prelude.Applicative.Applicative f
--- constructor of Prelude.Cast.Cast ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {from : Type ./Prelude/Cast.idr.c1} -> {to : Type ./Prelude/Cast.idr.f1} -> (from -> to) -> Prelude.Cast.Cast from to
--- constructor of Decidable.Equality.DecEq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {t : Type ./Decidable/Equality.idr.f2} -> ((x1 : t) -> (x2 : t) -> Prelude.Basics.Dec (= t t x1 x2)) -> Decidable.Equality.DecEq t
--- constructor of Prelude.Enum ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 9, nt_unique = False} {a : Type ./Prelude.idr.d57} -> (a -> a) -> (a -> a) -> (a -> Prelude.Nat.Nat) -> (Prelude.Nat.Nat -> a) -> (a -> Prelude.Stream.Stream a) -> (a -> a -> Prelude.Stream.Stream a) -> (a -> a -> Prelude.List.List a) -> (a -> a -> a -> Prelude.List.List a) -> Prelude.Enum a
--- constructor of Prelude.Interfaces.Eq ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {ty : Type ./Prelude/Interfaces.idr.j2} -> (ty -> ty -> Prelude.Bool.Bool) -> (ty -> ty -> Prelude.Bool.Bool) -> Prelude.Interfaces.Eq ty
--- constructor of Prelude.Foldable.Foldable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {t : Type ./Prelude/Foldable.idr.c1 -> Type ./Prelude/Foldable.idr.f1} -> ((acc : Type ./Prelude/Foldable.idr.i1) -> (elem : Type ./Prelude/Foldable.idr.l1) -> (elem -> acc -> acc) -> acc -> t elem -> acc) -> ((acc11 : Type ./Prelude/Foldable.idr.u1) -> (elem12 : Type ./Prelude/Foldable.idr.x1) -> (acc11 -> elem12 -> acc11) -> acc11 -> t elem12 -> acc11) -> Prelude.Foldable.Foldable t
--- constructor of Prelude.Interfaces.Fractional ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {ty : Type ./Prelude/Interfaces.idr.w123} -> Prelude.Interfaces.Num ty -> (ty -> ty -> ty) -> (ty -> ty) -> Prelude.Interfaces.Fractional ty
--- constructor of Prelude.Functor.Functor ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {f : Type ./Prelude/Functor.idr.c1 -> Type ./Prelude/Functor.idr.f1} -> ((b : Type ./Prelude/Functor.idr.i1) -> (a : Type ./Prelude/Functor.idr.l1) -> (a -> b) -> f a -> f b) -> Prelude.Functor.Functor f
--- constructor of Prelude.Interfaces.Integral ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {ty : Type ./Prelude/Interfaces.idr.x128} -> Prelude.Interfaces.Num ty -> (ty -> ty -> ty) -> (ty -> ty -> ty) -> Prelude.Interfaces.Integral ty
--- constructor of Prelude.Interfaces.MaxBound ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {b : Type ./Prelude/Interfaces.idr.u121} -> Prelude.Interfaces.Ord b -> b -> Prelude.Interfaces.MaxBound b
--- constructor of Prelude.Interfaces.MinBound ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {b : Type ./Prelude/Interfaces.idr.a120} -> Prelude.Interfaces.Ord b -> b -> Prelude.Interfaces.MinBound b
--- constructor of Prelude.Monad.Monad ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {m : Type ./Prelude/Monad.idr.c1 -> Type ./Prelude/Monad.idr.f1} -> Prelude.Applicative.Applicative m -> ((a : Type ./Prelude/Monad.idr.j1) -> (b : Type ./Prelude/Monad.idr.m1) -> m a -> (a -> m b) -> m b) -> ((a10 : Type ./Prelude/Monad.idr.t1) -> m (m a10) -> m a10) -> Prelude.Monad.Monad m
--- constructor of Prelude.Algebra.Monoid ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {ty : Type ./Prelude/Algebra.idr.i2} -> Prelude.Algebra.Semigroup ty -> ty -> Prelude.Algebra.Monoid ty
--- constructor of Prelude.Interfaces.Neg ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 5, nt_unique = False} {ty : Type ./Prelude/Interfaces.idr.q100} -> Prelude.Interfaces.Num ty -> (ty -> ty) -> (ty -> ty -> ty) -> (ty -> ty) -> Prelude.Interfaces.Neg ty
--- constructor of Prelude.Interfaces.Num ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {ty : Type ./Prelude/Interfaces.idr.d92} -> (ty -> ty -> ty) -> (ty -> ty -> ty) -> (Integer -> ty) -> Prelude.Interfaces.Num ty
--- constructor of Prelude.Interfaces.Ord ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 9, nt_unique = False} {ty : Type ./Prelude/Interfaces.idr.x22} -> Prelude.Interfaces.Eq ty -> (ty -> ty -> Prelude.Interfaces.Ordering) -> (ty -> ty -> Prelude.Bool.Bool) -> (ty -> ty -> Prelude.Bool.Bool) -> (ty -> ty -> Prelude.Bool.Bool) -> (ty -> ty -> Prelude.Bool.Bool) -> (ty -> ty -> ty) -> (ty -> ty -> ty) -> Prelude.Interfaces.Ord ty
--- constructor of Language.Reflection.Quotable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {a : Type ./Language/Reflection.idr.a175} -> {t : Type ./Language/Reflection.idr.d175} -> t -> (a -> t) -> Language.Reflection.Quotable a t
--- constructor of Language.Reflection.ReflConst ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {a : Type ./Language/Reflection.idr.w137} -> (a -> Language.Reflection.Const) -> Language.Reflection.ReflConst a
--- constructor of Prelude.Algebra.Semigroup ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {ty : Type ./Prelude/Algebra.idr.z} -> (ty -> ty -> ty) -> Prelude.Algebra.Semigroup ty
--- constructor of Prelude.Show.Show ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {ty : Type ./Prelude/Show.idr.i6} -> (ty -> String) -> (Prelude.Show.Prec -> ty -> String) -> Prelude.Show.Show ty
--- constructor of Prelude.Traversable.Traversable ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 4, nt_unique = False} {t : Type ./Prelude/Traversable.idr.q10 -> Type ./Prelude/Traversable.idr.t10} -> Prelude.Functor.Functor t -> Prelude.Foldable.Foldable t -> ((f : Type ./Prelude/Traversable.idr.y10 -> Type ./Prelude/Traversable.idr.b11) -> (b : Type ./Prelude/Traversable.idr.e11) -> (a : Type ./Prelude/Traversable.idr.h11) -> Prelude.Applicative.Applicative f -> (a -> f b) -> t a -> f (t b)) -> Prelude.Traversable.Traversable t
--- constructor of Prelude.Uninhabited.Uninhabited ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 2, nt_unique = False} {t : Type ./Prelude/Uninhabited.idr.z} -> (t -> Void) -> Prelude.Uninhabited.Uninhabited t
--- constructor of Prelude.WellFounded.WellFounded ---
RigCount: RigW
Injectivity: False
Accessibility: public export
Totality: Total
MetaInformation: EmptyMI
---
TyDecl: DCon {nt_tag = 0, nt_arity = 3, nt_unique = False} {a : Type ./Prelude/WellFounded.idr.t4} -> {rel : a -> a -> Type ./Prelude/WellFounded.idr.y4} -> ((x : a) -> Prelude.WellFounded.Accessible a rel x) -> Prelude.WellFounded.WellFounded a rel
*/
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment