h&#aH  Safe-Inferred5 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. Safe-Inferred5  Safe-Inferred7899#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!IJKLMN#"$O.-,+*)('&%P/Q98765431R20:S;?@A Safe-Inferred)[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ Safe-InferredSit#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.IdU Safe-Inferred vSitEncode a Haskell String to a list of Word8 values, in UTF8 format. Safe-Inferred ,9 9   Safe-Inferred SitThe printer class does the job.SitThe top-level printing method.   Safe-Inferred 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   Safe-Inferred 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.  Safe-Inferred 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.: Safe-Inferred>Sit&Type-check file given by command line.SitHandle error by failing hard.Sit+Run the type checker on file given by path.Sit0Run the type checker on text/contents of a file.  !"#"$"%&'()*+,-./0123456789:;<=>?@ABCDEF=>GHIJKLMNOPQR-ST./UVWXYZ[\G]^_`abcdefghi43EDCBA@>jkZ?lmnopqrHstuvwxFyzz{{|}~                                                                                                                                                    Sit-0.2022.3.18-inplaceSit ImpossibleLensInternalSit.AbsAbstractSit.LexSit.Par Sit.Print Substitute Evaluation TypeCheckermain checkFilecheckthrowImpossibledt-lns-lght-0.1.2.3-54ccc26fData.Lens.Light.Core^.getLisolensmodLmodL'setL vanLaarhovenData.Lens.Light.State!%=!=%=accesszoom~=Data.Lens.Light.TemplatemakeLens makeLenses nameMakeLensrunLens MonadStateToversetuse_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 failOnErr