h$"  Safe-Inferred3 Sit7We reached a program point which should be unreachable.SitAbort by throwing an "impossible" error. You should not use this function directly. Instead use the macro in  undefined.h.None, None567'#Sit!Relevance lattice (order matters) SitArgument decoration.!SitFunction domain decoration."Sit2Actual abstraction (body contains one more index).#Sit*No abstraction (argument will be ignored).$Sit Abstraction.%SitFunction application.&SitCase distinction'Sit Recursion(Sit T : Nat (b + 1) -> Set)Sit  tz : T zero*SitType of caseSuc0. Stored here for convenience, must be (t : Nat b) -> T (suc t)+Sit ts : (t : Nat b) -> T (suc t),Sit !T : ..(i : Size) -> Nat i -> Set-SitType of fixBody). Stored here for convenience, must be .(i : Size) (f : (x : Nat i) -> T i x) (x : Nat (i + 1)) -> T (i + 1) x..Sit t : .(i : Size) (f : (x : Nat i) -> T i x) (x : Nat (i + 1)) -> T (i + 1) x/Sit Eliminations.0SitUniverse with level.1Sit"Type of sizes (internal use only).2SitSized natural number type.3Sit%Zero constructor, or zero size (then Size is ignored).4Sit/Successor constructor, or successor size (then Size is ignored).5SitInfinity size.6SitLambda abstraction7Sit Variable.8SitFunction call.9SitApplication/eliminiation.:Sit Terms/types;SitSize expressions.<Sit Variables are de Bruijn indices.=SitDefinition names are strings.>Sit Zero size.?SitSuccessor size.@SitSize increment.ASit 'fixKind = ..(i : Size) -> Nat i -> Set<BCDE FGH!IJKL#"MN$O'&%.-,+*)(P/Q9765431R280:S;?@ANone)[\]^_`abcdefghijklmnopqrstuvwxyz{|}~NoneSit#Gather applications to expose head.Sit'Can this expression only denote a type?Sit#Is this expression an introduction?Sit-Convert "identifier-or-underscore" to string.Sit/Try to convert an expression to a list of A.IdUNone ISitEncode a Haskell String to a list of Word8 values, in UTF8 format.None> 9 9  None> SitThe printer class does the job.SitThe top-level printing method.  None> Sit.Substitution for various syntactic categories.Sit!Substitutions are lists of terms.SitWeakening substitution . E wkS || : SitIdentity substitution   E idS : .SitComposing substitution  A E  : A A E  : A ------------------------- A E compS   : A SitExtending a substitution   E  :   E T  E t : T --------------------------------  E consS t  : .T Sit*Lifting a substitution under a binder.   E  :   E T -------------------- .T E liftS  : .T SitWeakening a substitution.   E  :   E T ------------------ .T E weakS  :  Sit&Looking up an entry in a substitution.Sit-Construct the type of the functional for fix.@fixType t = .(i : Size) -> ((x : Nat i) -> T i x) -> (x : Nat (i + 1)) -> T (i + 1) x  None >SitAn environment maps de Bruijn indices to values. The first entry in the list is the binding for index 0.SitLambda abstractionSit x -> x e for internal use in fix.Sit Neutrals.Sit+Type annotation for readback (normal form).Sit Nat i -> SetSit!Size values are partially orderedSit&Compute predecessor size, if possible. None >{SitTyping context.SitDefault environment.Sit Local contextSitType errors are just strings.Sit Global stateSitExtending the typing contextSitThe type checking monadSitCheck a type signature.SitCheck a definition.Sit Check well-formedness of a type.Sit Nat i -> Nat i -> Nat i Sit'Semi-continuity check (to be completed)SitFor a function type to be upper semi-continuous, its codomain needs to be so, and the domain needs to be lower semi-continous.Sit8Base types and antitone types are lower semi-continuous.:NoneSit&Type-check file given by command line.Sit+Run the type checker on file given by path.Sit0Run the type checker on text/contents of a file.  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEF=>GHIJKLMNOP-QR.ST/UVWXYZ[G\]^_`abcdefghi43DCBA@>jkZ?lEmnopqrHstuvwxFyzz{{|}~                                                                                                                                                    &Sit-0.2021.1.18-HzrJgECr15PI6gfl38ib2tSit ImpossibleLensInternalSit.AbsAbstractSit.LexSit.Par Sit.Print Substitute Evaluation TypeCheckermain checkFilecheckthrowImpossible.data-lens-light-0.1.2.2-1M0z9JRubOM4qUVMmuptkHData.Lens.Light.Template nameMakeLensmakeLens makeLensesData.Lens.Light.Statezoom!%=%=!=~=access MonadStateTData.Lens.Light.Core vanLaarhoven^.modL'modLsetLgetLisolensrunLensoversetuse_2 RelevanceArgDomAbsNoAbsAbsNameApplyCaseFix caseReturncaseZero caseTySuccaseSuc fixReturn fixTyBodyfixBodyElimsTypeSizeNatZeroSucInftyPiLamVarDefIndexIdsZerosSucsPlusfixKindShapeIrrRelevant IrrelevantArgInfounArgargInfounDom_domInfoabsBodyabsNameElim'ElimTermAppLeveldbIndexdomInfozerosuc defaultArg defaultDomExpELamPlusForallLSucLZeroSet2Set1SetArrowIntBindBAnnBRelBIrrelIdUUnderQualIdConsSgDeclBlankOpenSigPrgIdentappView mustBeType introductionfromIdU parseIdUs utf8EncodeAlexAcc AlexAccSkip AlexAccNone AlexLastAcc AlexLastSkipAlexNone AlexReturn AlexTokenAlexSkip AlexErrorAlexEOFAlexAddrAlexA# AlexInputBytePosnPnBTreeBNTokenErrPTTokTCTDTVTITLTS alex_tab_size alex_base alex_table alex_check alex_deflt alex_accept alex_actionstok printPosntokenPos tokenPosn tokenLineCol posLineCol mkPosToken tokenTextprTokeneitherResIdentresWordsunescapeInitTail alexStartPosalexMovetokens alexGetBytealexInputPrevChar alex_action_3 alex_action_4 alex_action_5alexIndexInt16OffAddralexIndexInt32OffAddr quickIndexalexScan alexScanUser alex_scan_tknpPrgpDeclpQualId pListDeclpIdUpBind pListBind pListIdentpListIdUpExp2pExp1pExp happyErrormyLexerHappyStkPrint printTreeprtListprtDocdocrenderparenthconcatSconcatD replicateSmkEscprPrecSubstwkSidScompSconsSliftSweakSlookupSfixTypesubstraiseEnvVLamVElimByVUpVDownVSizeVGenReadback MonadEvalSizeViewSVConstSVVarSVInftyvVarvsZerovsSucvsVarvsPlusvsConstsvSucsizeViewmaxSizeevalInapply applyClos unfoldFix elimNeNatfixKindVcmpSizessizePredVClosclosEnvclosBodyVNe_neElims_neVarValVPiVInftyVSucVZeroVNatVTypeVElimsVElimVLevelreadbackEvaluateevalgetDefneVarneElims unSizeViewevaluateClosedapplyEsapplyE readbackType readbackNat readbackNe readbackSizeleqSize_envCxt_envEnvCxt TypeErrorTCSt AddContextCheckcheckSigcheckDef checkType inferTypeinferExpinferIdcoerce traceCheck lookupTySig lookupCxtlastVal resurrect admissibleadmissibleSemi upperSemi lowerSemiTCEnv_stDefs _stTySigsenvCxtenvEnv addContextstTySigsstDefs typeCheck checkDecls checkDecl inferPisType inferPiType checkSize checkLevelcheckExpinferNatnyi lookupDefaddTySigaddDefevaluate applyClosure applyElims applyArgs reifyType reifySizesubType equalTypedebugmonotone monotoneSize debugSize