Index
Symbols
A
AR(environment variable)AccAcc.intro AccessRightAddAdd.mk AddRightCancelAlternativeAlternative.mk AndAnd.elim And.intro AndOpAndOp.mk AppendAppend.mk ApplicativeApplicative.mk ArrayArray.all Array.allDiff Array.allM Array.any Array.anyM Array.append Array.appendList Array.attach Array.attachWith Array.back Array.back! Array.back? Array.binInsert Array.binInsertM Array.binSearch Array.binSearchContains Array.contains Array.count Array.countP Array.drop Array.elem Array.empty Array.emptyWithCapacity Array.erase Array.eraseIdx Array.eraseIdx! Array.eraseIdxIfInBounds Array.eraseP Array.eraseReps Array.extract Array.filter Array.filterM Array.filterMap Array.filterMapM Array.filterRevM Array.filterSepElems Array.filterSepElemsM Array.finIdxOf? Array.finRange Array.find? Array.findFinIdx? Array.findIdx Array.findIdx? Array.findIdxM? Array.findM? Array.findRev? Array.findRevM? Array.findSome! Array.findSome? Array.findSomeM? Array.findSomeRev? Array.findSomeRevM? Array.firstM Array.flatMap Array.flatMapM Array.flatten Array.foldl Array.foldlM Array.foldr Array.foldrM Array.forM Array.forRevM Array.getD Array.getEvenElems Array.getMax? Array.groupByKey Array.idxOf Array.idxOf? Array.insertIdx Array.insertIdx! Array.insertIdxIfInBounds Array.insertionSort Array.isEmpty Array.isEqv Array.isPrefixOf Array.iter Array.iterFromIdx Array.iterFromIdxM Array.iterM Array.leftpad Array.lex Array.map Array.mapFinIdx Array.mapFinIdxM Array.mapIdx Array.mapIdxM Array.mapM Array.mapM' Array.mapMono Array.mapMonoM Array.mk Array.modify Array.modifyM Array.modifyOp Array.ofFn Array.ofSubarray Array.partition Array.pmap Array.pop Array.popWhile Array.push Array.qsort Array.qsortOrd Array.range Array.range' Array.replace Array.replicate Array.reverse Array.rightpad Array.set Array.set! Array.setIfInBounds Array.shrink Array.singleton Array.size Array.sum Array.swap Array.swapAt Array.swapAt! Array.swapIfInBounds Array.take Array.takeWhile Array.toList Array.toListAppend Array.toListRev Array.toSubarray Array.toVector Array.uget Array.unattach Array.unzip Array.uset Array.usize Array.zip Array.zipIdx Array.zipWith Array.zipWithAll AssertionAssertionAssociativeAsyncAsyncReadAsyncStreamAsyncTaskAsyncWriteAtomicTabsabsabsabsabsabsabsabsabsabsurdacacac_nfac_nf0ac_rflacceptacceptSelectoraccessedacosacosacoshacoshadaptadaptadaptExceptadcadcbaddaddaddaddaddaddaddaddaddaddaddaddaddaddaddaddaddaddaddAppParenaddCasesaddEnvLinterOptionaddExtensionaddHeartbeatsaddLinteraddMacroScopeaddModuleLinteraddNatadd_assocadd_commadd_le_left_iffadd_one_nsmuladd_right_canceladd_zeroadd_zsmuladmit(0) (1)allallallallallallallallallallallallallallallDiffallEqallIallMallMallMallMallMallMallOnesallTRall_goals(0) (1) (2)allowImportAllallowUnsafeReducibilityalteralteralteralteralteralteralternativeandandandandandandandandandMand_introsanyanyanyanyanyanyanyanyanyanyanyanyanyIanyManyManyManyManyManyManyTRany_goals(0) (1) (2)appDirappPathappendappendappendappendappendappendappendListappendTRapply(0) (1) (2)applyapply?apply_assumptionapply_ext_theoremapply_mod_castapply_rflapply_rulesarg [@]iargsargsargsaritharrayarrayasTaskasTaskasTaskasTaskasTaskas_aux_lemmaasinasinasinhasinhassertassocassumption- assumption
assumption_mod_castasyncasyncatatEndatEndatEndatEndatIdx!atIdxatIdx?atIdx?atIdx?atIdxDatIdxSlow?atanatanatan2atan2atanhatanhatomicallyatomicallyOnceattachattachattachattachWithattachWithattachWithattachWithattachWithautoImplicitautoLiftautoParamautoPromoteIndicesautoUnfoldautoUnfoldawaitawaitCancellation
B
BEqBEq.mk BackendBacktrackableBackwardPatternBaseAsyncBaseIOBaseIO.asTask BaseIO.bindTask BaseIO.chainTask BaseIO.mapTask BaseIO.mapTasks BaseIO.toEIO BaseIO.toIO BindBind.bindLeft Bind.kleisliLeft Bind.kleisliRight Bind.mk BitVecBitVec.abs BitVec.adc BitVec.adcb BitVec.add BitVec.allOnes BitVec.and BitVec.append BitVec.carry BitVec.cast BitVec.concat BitVec.cons BitVec.decEq BitVec.divRec BitVec.divSubtractShift BitVec.extractLsb BitVec.extractLsb' BitVec.fill BitVec.getLsb BitVec.getLsb? BitVec.getLsbD BitVec.getMsb BitVec.getMsb? BitVec.getMsbD BitVec.hash BitVec.intMax BitVec.intMin BitVec.iunfoldr BitVec.iunfoldr_replace BitVec.msb BitVec.mul BitVec.mulRec BitVec.neg BitVec.nil BitVec.not BitVec.ofBool BitVec.ofBoolListBE BitVec.ofBoolListLE BitVec.ofFin BitVec.ofInt BitVec.ofNat BitVec.ofNatLT BitVec.or BitVec.replicate BitVec.reverse BitVec.rotateLeft BitVec.rotateRight BitVec.saddOverflow BitVec.sdiv BitVec.setWidth BitVec.setWidth' BitVec.shiftConcat BitVec.shiftLeft BitVec.shiftLeftRec BitVec.shiftLeftZeroExtend BitVec.signExtend BitVec.sle BitVec.slt BitVec.smod BitVec.smtSDiv BitVec.smtUDiv BitVec.srem BitVec.sshiftRight BitVec.sshiftRight' BitVec.sshiftRightRec BitVec.ssubOverflow BitVec.sub BitVec.toHex BitVec.toInt BitVec.toNat BitVec.truncate BitVec.twoPow BitVec.uaddOverflow BitVec.udiv BitVec.ule BitVec.ult BitVec.umod BitVec.ushiftRight BitVec.ushiftRightRec BitVec.usubOverflow BitVec.xor BitVec.zero BitVec.zeroExtend BoolBool.and Bool.dcond Bool.decEq Bool.false Bool.not Bool.or Bool.toISize Bool.toInt Bool.toInt16 Bool.toInt32 Bool.toInt64 Bool.toInt8 Bool.toNat Bool.toUInt16 Bool.toUInt32 Bool.toUInt64 Bool.toUInt8 Bool.toUSize Bool.true Bool.xor BufferBuildTypeByteArrayByteArray.Iterator ByteArray.Iterator. atEnd ByteArray.Iterator. curr ByteArray.Iterator. curr' ByteArray.Iterator. forward ByteArray.Iterator. hasNext ByteArray.Iterator. hasPrev ByteArray.Iterator. mk ByteArray.Iterator. next ByteArray.Iterator. next' ByteArray.Iterator. nextn ByteArray.Iterator. pos ByteArray.Iterator. prev ByteArray.Iterator. prevn ByteArray.Iterator. remainingBytes ByteArray.Iterator. toEnd ByteArray.append ByteArray.copySlice ByteArray.empty ByteArray.emptyWithCapacity ByteArray.extract ByteArray.fastAppend ByteArray.findFinIdx? ByteArray.findIdx? ByteArray.foldl ByteArray.foldlM ByteArray.forIn ByteArray.get ByteArray.get! ByteArray.isEmpty ByteArray.iter ByteArray.mk ByteArray.push ByteArray.set ByteArray.set! ByteArray.size ByteArray.toByteSlice ByteArray.toList ByteArray.toUInt64BE! ByteArray.toUInt64LE! ByteArray.uget ByteArray.uset ByteArray.usize ByteArray.utf8Decode? ByteArray.utf8DecodeChar ByteArray.utf8DecodeChar? ByteSliceByteSlice.beq ByteSlice.byteArray ByteSlice.contains ByteSlice.empty ByteSlice.foldr ByteSlice.foldrM ByteSlice.forM ByteSlice.get ByteSlice.get! ByteSlice.getD ByteSlice.ofByteArray ByteSlice.size ByteSlice.slice ByteSlice.start ByteSlice.stop ByteSlice.toByteArray back!backbackbackback?back?backgroundbackgroundbackward.do. legacy backward.inferInstanceAs. wrap backward.inferInstanceAs. wrap. data backward.inferInstanceAs. wrap. instances backward.inferInstanceAs. wrap. reuseSubInstances backward.privateInPublic backward.privateInPublic. warn backward.proofsInPublic backward.synthInstance. canonInstances baseIdbasisbdivbeginbeqbeqbeqbeqbeqbeqbeqbeqbeqbetabetabientailsbinInsertbinInsertMbinSearchbinSearchContainsbindbindbindbindbindbindbindbindbindbindbindbindbindbindbindbindbindContbindIObindLeftbindMbindTaskbindTaskbindTaskbind_assocbind_le_wp_bindbind_mapbind_pure_compbinderNameHintbitVecOfNatbitwisebleblockblockblockblockbltbmodbootstrap.inductiveCheckResultingUniverse bracketbracketFillbreakBase?breakContbreaksbsizebucketsbuild(Lake command)bv_check(0) (1)bv_decide(0) (1)bv_decide?(0) (1)bv_normalize(0) (1)bv_omegabyCasesby_casesby_cases'by_casesby_contrabytebytebyteArraybyteDistancebyteIdxbyteSizebytes
C
CC(environment variable)CCPOCOMPARATOR_BWRAP(environment variable)CancellationContextCancellationReasonCancellationTokenChannelCharChar.isAlpha Char.isAlphanum Char.isDigit Char.isLower Char.isUpper Char.isValidCharNat Char.isWhitespace Char.le Char.lt Char.mk Char.ofNat Char.ofUInt8 Char.quote Char.toLower Char.toNat Char.toString Char.toUInt8 Char.toUpper Char.utf8Size CharLitChildClientCloseableChannelCodeLivenessCoeCoe.mk CoeDepCoeDep.mk CoeFunCoeFun.mk CoeHTCCoeHTC.mk CoeHTCTCoeHTCT.mk CoeHeadCoeHead.mk CoeOTCCoeOTC.mk CoeOutCoeOut.mk CoeSortCoeSort.mk CoeTCoeT.mk CoeTCCoeTC.mk CoeTailCoeTail.mk CommRingCommSemiringCommandCommutativeCompleteLatticeCondvarConfigConfigConfigConjunctiveConsumerContInfoContextContextAsyncControlInfoControlInfoHandlerCursorcache add(Lake command)cache clean(Lake command)cache get(Lake command)cache put(Lake command)cache put-staged(Lake command)cache services(Lake command)cache stage(Lake command)cache unstage(Lake command)cachedPUnitcachedPUnitUnitcalc- call-by-need
cancelcancelcancelcancelledcanonInstancescapitalizecarrycase(0) (1)case ...=> ... case'case' ...=> ... caseStrongRecOncases(0) (1)casescases?casesAuxOncases_nextcastcastcastcastcastcastcastcastAddcastLEcastLTcastSucccast_heqcatchExceptionscatchRuntimecbrtcbrtcbv(0) (1) (2)cbv.maxSteps cbv.warning ceilceil- chain
chainTaskchainTaskchainTaskchange(0) (1)charLitKindcharscheck(Lake command)check-build(Lake command)check-lint(Lake command)check-test(Lake command)checkCanceledcheckFinishedchoicechoiceKindchooseclassicalclean(Lake command)clearclear_valuecmdcoecoecoecoecoecoecoecoecoecoecoecoecolEqcolGecolGtcombinecomm- comment
- comment
commonPrefixcommonSuffixcompcomp_mapcomparator(Lake command)comparecomparecompareLexcompareOfLessAndBEqcompareOfLessAndEqcompareOncomplementcomplementcomplementcomplementcomplementcomplementcomplementcomplementcomplementcomplementcompletions(Elan command)componentsconcatconcatconcurrentlyconcurrentlyconcurrentlyconcurrentlyconcurrentlyAllconcurrentlyAllconcurrentlyAllconcurrentlyAllcond- configuration
congr(0) (1) (2)congrArgcongrConstscongrFunconjunctionconjunctiveRawconnectconnectconsconst- constructor (0) (1)
consumerscontcontInfocontainscontainscontainscontainscontainscontainscontainscontainscontainscontainscontainscontainscontainscontainscontainscontainsThenInsertcontainsThenInsertcontainsThenInsertcontainsThenInsertcontainsThenInsertcontainsThenInsertcontainsThenInsertcontainsThenInsertcontainsThenInsertcontainsThenInsertIfNewcontainsThenInsertIfNewcontainsThenInsertIfNewcontainsThenInsertIfNewcontainsThenInsertIfNewcontainsThenInsertIfNewcontextualcontinueBase?continueContcontinueWithUnitcontinuescontradictioncontrolcontrolAtconvconv => ...conv'(0) (1)copycopycopySlicecoreInternalcoscoscoshcoshcountcountcountPcountPcreateDircreateDirAllcreateTempDircreateTempFilecrlfToLf- cumulativity
curr'curr'currcurrcurrColumncurrentcurrentDircurrycurrycustomEliminatorscwd
D
DHashMapDTreeMapDecidableDecidable.byCases Decidable.decide Decidable.intro DecidableEqDecidableLEDecidableLTDecidablePredDecidableRelDirEntryDivDiv.mk DoElabDoElemContDoElemContKindDoOpsDvdDvd.mk datadatadatadbg_tracedconddeadCodedecdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecEqdecLedecLedecLedecLedecLedecLedecLedecLedecLedecLedecLedecLedecLedecLtdecLtdecLtdecLtdecLtdecLtdecLtdecLtdecLtdecLtdecLtdecLtdecLtdecapitalize- decidable
decidableEqNonedecidedecidedecidedecidedecidedecide_cbvdeclareMutVardeclareMutVarsdecreaseBydecreasing_tacticdecreasing_trivialdecreasing_withdedicateddeepTermsdefIndentdefWidthdefault(Elan command)defaultdefaultdefaultFacetsdefaultImplementationdeflatedelta(0) (1)diffdigitChardiscarddischargedisowndivdivdivdivdivdivdivdivdivdivdivdivdivdivdivdivdiv2InductiondivRecdivSubtractShiftdiv_eq_mul_invdoBlockResultTypedone(0) (1) (2)donedonedoneSelectordoneSelectordowndowndraindropdropdropdropdropdropdropdropdropEnddropEnddropEndWhiledropEndWhiledropLastdropLastTRdropPrefixdropPrefixdropPrefix?dropPrefix?dropPrefix?dropRightdropRightWhiledropSuffixdropSuffixdropSuffix?dropSuffix?dropSuffix?dropWhiledropWhiledropWhiledropWhiledropWhiledropWhiledropWhileMdropWhileWithPostconditiondsimp(0) (1) (2)dsimp!dsimpdsimp?dsimp?!dvd
E
EAsyncEIOEIO.asTask EIO.bindTask EIO.catchExceptions EIO.chainTask EIO.mapTask EIO.mapTasks EIO.toBaseIO EIO.toIO EIO.toIO' ELAN(environment variable)ELAN_HOME(environment variable)ESTEStateMEStateM.Backtrackable EStateM.Backtrackable. mk EStateM.Result EStateM.Result. error EStateM.Result. ok EStateM.adaptExcept EStateM.bind EStateM.fromStateM EStateM.get EStateM.map EStateM.modifyGet EStateM.nonBacktrackable EStateM.orElse EStateM.orElse' EStateM.pure EStateM.run EStateM.run' EStateM.seqRight EStateM.set EStateM.throw EStateM.tryCatch ETaskEffectForwarderEmptyEmpty.elim EntryEnvLinterEqEq.mp Eq.mpr Eq.refl Eq.subst Eq.symm Eq.trans EquivEquivEquivEquivEquivEquivEquivBEqEquivBEq.mk EquivalenceEquivalence.mk ErrorEvenEven.plusTwo Even.zero ExceptExcept.bind Except.error Except.isOk Except.map Except.mapError Except.ok Except.orElseLazy Except.pure Except.toBool Except.toOption Except.tryCatch ExceptCondsExceptCpsTExceptCpsT.lift ExceptCpsT.run ExceptCpsT.runCatch ExceptCpsT.runK ExceptTExceptT.adapt ExceptT.bind ExceptT.bindCont ExceptT.lift ExceptT.map ExceptT.mk ExceptT.pure ExceptT.run ExceptT.tryCatch ExistsExists.choose Exists.intro ExtDHashMapExtHashMapExtHashSetedivelabAsSyntacticallyDeadCodeelabDoElemelabDoElems1elabDoSeqelemelemelemsAndSepselemsAndSepselimelimelimelimelimelimelimelimelimelimelim0elimMemodemptyemptyemptyemptyemptyemptyemptyemptyemptyemptyemptyWithCapacityemptyWithCapacityemptyWithCapacityemptyWithCapacityemptyWithCapacityemptyWithCapacityemptyWithCapacityemptyWithCapacityendendExclusiveendPosendPosendTagsendsWithendsWithendsWithensureHasTypeAtensureTerminationensureTerminationensureUnitensureUnitAtentailsentailsenterenterLoopBodyentryAtIdx!entryAtIdxentryAtIdx?entryAtIdxDenv(Lake command)env- environment variables
eprinteprintlneqIgnoreAsciiCaseeqRec_heqeq_of_beqeq_of_heqeq_of_succ?_eqeq_refleraseeraseeraseeraseeraseeraseeraseeraseeraseeraseeraseeraseDupseraseIdx!eraseIdxeraseIdxeraseIdxIfInBoundseraseIdxTReraseManyeraseManyerasePerasePerasePTReraseRepseraseRepseraseTRerasederrorsFounderw(0) (1)etaetaetaStructetaStructeval.derive. repr eval.pp eval.type exact(0) (1)exactexact?exact_mod_castexe(Lake command)exeExtensionexeNameexecutionexfalsoexistsexistsexitexitCodeexpexpexp2exp2expandMacro?expose_names(0) (1)ext(0) (1)ext1extSeparatorextension- extensionality
extraextraDepTargetsextractextractextractextractextractextractextractextractLsb'extractLsbextract_lets
F
FalseFalse.elim FieldFilePathFileRightFinFin.add Fin.addCases Fin.addNat Fin.cases Fin.cast Fin.castAdd Fin.castLE Fin.castLT Fin.castSucc Fin.div Fin.elim0 Fin.foldl Fin.foldlM Fin.foldr Fin.foldrM Fin.hIterate Fin.hIterateFrom Fin.induction Fin.inductionOn Fin.land Fin.last Fin.lastCases Fin.log2 Fin.lor Fin.mk Fin.mod Fin.modn Fin.mul Fin.natAdd Fin.ofNat Fin.pred Fin.rev Fin.reverseInduction Fin.shiftLeft Fin.shiftRight Fin.sub Fin.subNat Fin.succ Fin.succRec Fin.succRecOn Fin.toNat Fin.xor FiniteFiniteFlattenBehaviorFloatFloat.Model Float.Model. UnpackedFloat Float.Model. UnpackedFloat. abs Float.Model. UnpackedFloat. add Float.Model. UnpackedFloat. beq Float.Model. UnpackedFloat. compare Float.Model. UnpackedFloat. div Float.Model. UnpackedFloat. finite Float.Model. UnpackedFloat. infinity Float.Model. UnpackedFloat. isFinite Float.Model. UnpackedFloat. isInf Float.Model. UnpackedFloat. isNaN Float.Model. UnpackedFloat. le Float.Model. UnpackedFloat. lt Float.Model. UnpackedFloat. mul Float.Model. UnpackedFloat. neg Float.Model. UnpackedFloat. notANumber Float.Model. UnpackedFloat. ofISize Float.Model. UnpackedFloat. ofInt Float.Model. UnpackedFloat. ofInt16 Float.Model. UnpackedFloat. ofInt32 Float.Model. UnpackedFloat. ofInt64 Float.Model. UnpackedFloat. ofInt8 Float.Model. UnpackedFloat. ofNat Float.Model. UnpackedFloat. ofScientific Float.Model. UnpackedFloat. ofUInt16 Float.Model. UnpackedFloat. ofUInt32 Float.Model. UnpackedFloat. ofUInt64 Float.Model. UnpackedFloat. ofUInt8 Float.Model. UnpackedFloat. ofUSize Float.Model. UnpackedFloat. sqrt Float.Model. UnpackedFloat. sub Float.Model. UnpackedFloat. toISize Float.Model. UnpackedFloat. toInt16 Float.Model. UnpackedFloat. toInt32 Float.Model. UnpackedFloat. toInt64 Float.Model. UnpackedFloat. toInt8 Float.Model. UnpackedFloat. toUInt16 Float.Model. UnpackedFloat. toUInt32 Float.Model. UnpackedFloat. toUInt64 Float.Model. UnpackedFloat. toUInt8 Float.Model. UnpackedFloat. toUSize Float.Model. UnpackedFloat. zero Float.Model. mk Float.Model. pack Float.Model. unpack Float.abs Float.acos Float.acosh Float.add Float.asin Float.asinh Float.atan Float.atan2 Float.atanh Float.beq Float.cbrt Float.ceil Float.cos Float.cosh Float.decLe Float.decLt Float.div Float.exp Float.exp2 Float.floor Float.frExp Float.isFinite Float.isInf Float.isNaN Float.le Float.log Float.log10 Float.log2 Float.lt Float.mul Float.neg Float.ofBits Float.ofInt Float.ofModel Float.ofNat Float.pow Float.round Float.scaleB Float.sin Float.sinh Float.sqrt Float.sub Float.tan Float.tanh Float.toBits Float.toFloat32 Float.toISize Float.toInt16 Float.toInt32 Float.toInt64 Float.toInt8 Float.toString Float.toUInt16 Float.toUInt32 Float.toUInt64 Float.toUInt8 Float.toUSize Float32Float32.Model Float32.Model. mk Float32.Model. pack Float32.Model. unpack Float32.abs Float32.acos Float32.acosh Float32.add Float32.asin Float32.asinh Float32.atan Float32.atan2 Float32.atanh Float32.beq Float32.cbrt Float32.ceil Float32.cos Float32.cosh Float32.decLe Float32.decLt Float32.div Float32.exp Float32.exp2 Float32.floor Float32.frExp Float32.isFinite Float32.isInf Float32.isNaN Float32.le Float32.log Float32.log10 Float32.log2 Float32.lt Float32.mul Float32.neg Float32.ofBits Float32.ofInt Float32.ofModel Float32.ofNat Float32.pow Float32.round Float32.scaleB Float32.sin Float32.sinh Float32.sqrt Float32.sub Float32.tan Float32.tanh Float32.toBits Float32.toFloat Float32.toISize Float32.toInt16 Float32.toInt32 Float32.toInt64 Float32.toInt8 Float32.toString Float32.toUInt16 Float32.toUInt32 Float32.toUInt64 Float32.toUInt8 Float32.toUSize ForInForIn'ForIn'.mk ForIn.mk ForInStepForInStep.done ForInStep.value ForInStep.yield ForMForM.forIn ForM.mk FormatForwardPatternFunction.HasLeftInverse Function.HasRightInverse Function.Injective Function.LeftInverse Function.RightInverse Function.Surjective Function.comp Function.const Function.curry Function.uncurry FunctorFunctor.discard Functor.mapRev Functor.mk fail(0) (1)failfailIfUnchangedfailIfUnchangedfail_if_success(0) (1) (2)failurefailurefailurefalse_or_by_contrafastAppendfdivfieldIdxKindfieldNotationfileNamefileNamefileStemfillfillfilterfilterfilterfilterfilterfilterfilterfilterfilterfilterfilterfilterfilterfilterfilterMfilterMfilterMfilterMfilterMfilterMapfilterMapfilterMapfilterMapfilterMapfilterMapfilterMapfilterMapfilterMapfilterMapfilterMapMfilterMapMfilterMapMfilterMapMfilterMapTRfilterMapWithPostconditionfilterMapWithPostconditionfilterRevMfilterRevMfilterSepElemsfilterSepElemsMfilterTRfilterWithPostconditionfilterWithPostconditionfinIdxOf?finIdxOf?finRangefinRangefindfindfind?find?find?find?find?findCodeQualitySourcefindCodeQualitySource?findExternLib?findFinIdx?findFinIdx?findFinIdx?findIdxfindIdxfindIdx?findIdx?findIdx?findIdxM?findLeanExe?findLeanLib?findM?findM?findM?findM?findMatchingDecl?findModule?findPackageByKey?findPackageByName?findRev?findRev?findRevM?findRevM?findSome!findSome?findSome?findSome?findSome?findSomeM?findSomeM?findSomeM?findSomeM?findSomeRev?findSomeRevM?findSomeRevM?finishfinish?finishedfinitefinitefinitelyManySkipsfinitelyManySkipsfinitelyManyStepsfinitelyManyStepsfirst(0) (1) (2)firstDiffPosfirstMfirstMfixfixfix_eqflagsflagsflatMapflatMapflatMapflatMapflatMapAfterflatMapAfterflatMapAfterMflatMapAfterMflatMapMflatMapMflatMapMflatMapMflatMapTRflattenflattenflattenTRfloorfloorflushflushflushfmodfnfocus(0) (1) (2)foldfoldfoldfoldfoldfoldfoldIfoldMfoldMfoldMfoldMfoldMfoldMfoldRevfoldRevMfoldTRfoldUntilfoldlfoldlfoldlfoldlfoldlfoldlfoldlfoldlfoldlfoldlfoldlMfoldlMfoldlMfoldlMfoldlMfoldlMfoldlMfoldlRecOnfoldrfoldrfoldrfoldrfoldrfoldrfoldrfoldrfoldrfoldrfoldrMfoldrMfoldrMfoldrMfoldrMfoldrMfoldrMfoldrRecOnfoldrTRforAforAsyncforIn'forInforInforInforInforInforInforInforInforInforInforInforMforMforMforMforMforMforMforMforMforMforMforMforMforRevMforRevMforRevMforallforkformatformatforwardforwardfrExpfrExpfromStateMfromUTF8!fromUTF8fromUTF8?frontfrontfrontfront?fstfstfstfstfstfunfun_casesfun_inductionfunext(0) (1)
G
GetElemGetElem.mk GetElem?GetElem?.mk Globgcdgcdgeneralizeget!get!get!get!get!get!get!get!get!get!get!get!get!get!get!get!get'getgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetgetget?get?get?get?get?get?get?get?get?get?get?get?getAddrInfogetAugmentedEnvgetAugmentedLeanPathgetAugmentedLeanSrcPathgetBreakContgetCancellationReasongetCancellationReasongetChargetContextgetContinueContgetCurrNamespacegetCurrentDirgetDgetDgetDgetDgetDgetDgetDgetDgetDgetDgetDgetDgetDgetDgetDMgetElan?getElanHome?getElanInstall?getElanToolchaingetElem!getElem!_defgetElemgetElem?getElem?_defgetElemsgetEntryGE!getEntryGEgetEntryGE?getEntryGEDgetEntryGT!getEntryGTgetEntryGT?getEntryGTDgetEntryLE!getEntryLEgetEntryLE?getEntryLEDgetEntryLT!getEntryLTgetEntryLT?getEntryLTDgetEnvgetEnvLeanPathgetEnvLeanSrcPathgetEvenElemsgetGE!getGEgetGE?getGEDgetGT!getGTgetGT?getGTDgetHygieneInfogetIdgetKey!getKey!getKey!getKey!getKey!getKey!getKeygetKeygetKeygetKeygetKeygetKeygetKey?getKey?getKey?getKey?getKey?getKey?getKeyDgetKeyDgetKeyDgetKeyDgetKeyDgetKeyDgetKeyGE!getKeyGEgetKeyGE?getKeyGEDgetKeyGT!getKeyGTgetKeyGT?getKeyGTDgetKeyLE!getKeyLEgetKeyLE?getKeyLEDgetKeyLT!getKeyLTgetKeyLT?getKeyLTDgetKindgetLE!getLEgetLE?getLEDgetLT!getLTgetLT?getLTDgetLakegetLakeEnvgetLakeHomegetLakeInstallgetLakeLibDirgetLakeSrcDirgetLast!getLastgetLast?getLastDgetLeangetLeanArgetLeanCcgetLeanCc?getLeanIncludeDirgetLeanInstallgetLeanLibDirgetLeanPathgetLeanSrcDirgetLeanSrcPathgetLeanSysrootgetLeanSystemLibDirgetLeancgetLeftgetLeft?getLinegetLinegetLinterOptionsgetLinterValuegetLsbgetLsb?getLsbDgetMgetMax?getModifygetMsbgetMsb?getMsbDgetNamegetNameInfogetNatgetNoCachegetNumHeartbeatsgetPIDgetPeerNamegetPeerNamegetPkgUrlMapgetRandomBytesgetReturnContgetRightgetRight?getRootPackagegetScientificgetSockNamegetSockNamegetSockNamegetStategetStategetStderrgetStdingetStdoutgetStringgetTIDgetTaskStategetThegetThegetThenInsertIfNew?getThenInsertIfNew?getThenInsertIfNew?getThenInsertIfNew?getThenInsertIfNew?getThenInsertIfNew?getTryCachegetUTF8Byte!getUTF8BytegetUTF8BytegetWorkspaceget_elem_tacticget_elem_tactic_trivialglobs- goal
grindgrind?grobnergroundgroupgroupByKeygroupByKeygroupKindguardguardguard_exprguard_hypguard_msgs.diff guard_target
H
HAddHAdd.mk HAndHAnd.mk HAppendHAppend.mk HDivHDiv.mk HEqHEq.elim HEq.ndrec HEq.ndrecOn HEq.refl HEq.rfl HEq.subst HModHMod.mk HMulHMul.mk HOrHOr.mk HPowHPow.mk HShiftLeftHShiftLeft.mk HShiftRightHShiftRight.mk HSubHSub.mk HXorHXor.mk HandleHasEquivHasEquiv.mk HasLeftInverseHasRightInverseHasSizeHasSizeHashMapHashSetHashableHashable.mk HetTHomogeneousPowHomogeneousPow.mk HygieneInfohAddhAndhAppendhDivhIteratehIterateFromhModhMulhOrhPowhShiftLefthShiftRighthSubhXorhasDeclhasFinishedhasNexthasNexthasPrevhasPrevhas_csuphas_suphashhashhashhash_eqhash_eqhave(0) (1) (2)have'head!headhead?headDhelimheq_of_eqheq_of_eqRec_eqheq_of_heq_of_eqhomhosthrecOnhrecOn- hygiene
hygieneInfoKindhygienic
I
IOIO.AccessRight IO.AccessRight. flags IO.AccessRight. mk IO.Error IO.Error. alreadyExists IO.Error. hardwareFault IO.Error. illegalOperation IO.Error. inappropriateType IO.Error. interrupted IO.Error. invalidArgument IO.Error. noFileOrDirectory IO.Error. noSuchThing IO.Error. otherError IO.Error. permissionDenied IO.Error. protocolError IO.Error. resourceBusy IO.Error. resourceExhausted IO.Error. resourceVanished IO.Error. timeExpired IO.Error. toString IO.Error. unexpectedEof IO.Error. unsatisfiedConstraints IO.Error. unsupportedOperation IO.Error. userError IO.FS. DirEntry IO.FS. DirEntry. mk IO.FS. DirEntry. path IO.FS. Handle IO.FS. Handle. flush IO.FS. Handle. getLine IO.FS. Handle. isTty IO.FS. Handle. lock IO.FS. Handle. mk IO.FS. Handle. putStr IO.FS. Handle. putStrLn IO.FS. Handle. read IO.FS. Handle. readBinToEnd IO.FS. Handle. readBinToEndInto IO.FS. Handle. readToEnd IO.FS. Handle. rewind IO.FS. Handle. truncate IO.FS. Handle. tryLock IO.FS. Handle. unlock IO.FS. Handle. write IO.FS. Metadata IO.FS. Metadata. mk IO.FS. Mode IO.FS. Mode. append IO.FS. Mode. read IO.FS. Mode. readWrite IO.FS. Mode. write IO.FS. Mode. writeNew IO.FS. Stream IO.FS. Stream. Buffer IO.FS. Stream. Buffer. mk IO.FS. Stream. mk IO.FS. Stream. ofBuffer IO.FS. Stream. ofHandle IO.FS. Stream. putStrLn IO.FS. createDir IO.FS. createDirAll IO.FS. createTempDir IO.FS. createTempFile IO.FS. lines IO.FS. readBinFile IO.FS. readFile IO.FS. realPath IO.FS. removeDir IO.FS. removeDirAll IO.FS. removeFile IO.FS. rename IO.FS. withFile IO.FS. withIsolatedStreams IO.FS. withTempDir IO.FS. withTempFile IO.FS. writeBinFile IO.FS. writeFile IO.FileRight IO.FileRight. flags IO.FileRight. mk IO.Process. Child IO.Process. Child. kill IO.Process. Child. takeStdin IO.Process. Child. tryWait IO.Process. Child. wait IO.Process. Output IO.Process. Output. mk IO.Process. SpawnArgs IO.Process. SpawnArgs. mk IO.Process. Stdio IO.Process. Stdio. inherit IO.Process. Stdio. null IO.Process. Stdio. piped IO.Process. Stdio. toHandleType IO.Process. StdioConfig IO.Process. StdioConfig. mk IO.Process. exit IO.Process. getCurrentDir IO.Process. getPID IO.Process. output IO.Process. run IO.Process. setCurrentDir IO.Process. spawn IO.Promise IO.Promise. isResolved IO.Promise. new IO.Promise. resolve IO.Promise. result! IO.Promise. result? IO.Promise. resultD IO.Ref IO.TaskState IO.TaskState. finished IO.TaskState. running IO.TaskState. waiting IO.addHeartbeats IO.appDir IO.appPath IO.asTask IO.bindTask IO.cancel IO.chainTask IO.checkCanceled IO.currentDir IO.eprint IO.eprintln IO.getEnv IO.getNumHeartbeats IO.getRandomBytes IO.getStderr IO.getStdin IO.getStdout IO.getTID IO.getTaskState IO.hasFinished IO.iterate IO.lazyPure IO.mapTask IO.mapTasks IO.mkRef IO.monoMsNow IO.monoNanosNow IO.ofExcept IO.print IO.println IO.rand IO.setAccessRights IO.setRandSeed IO.setStderr IO.setStdin IO.setStdout IO.sleep IO.toEIO IO.userError IO.wait IO.waitAny IO.withStderr IO.withStdin IO.withStdout ISizeISize.abs ISize.add ISize.complement ISize.decEq ISize.decLe ISize.decLt ISize.div ISize.land ISize.le ISize.lor ISize.lt ISize.maxValue ISize.minValue ISize.mod ISize.mul ISize.neg ISize.ofBitVec ISize.ofInt ISize.ofIntClamp ISize.ofIntLE ISize.ofNat ISize.ofUSize ISize.shiftLeft ISize.shiftRight ISize.size ISize.sub ISize.toBitVec ISize.toFloat ISize.toFloat32 ISize.toInt ISize.toInt16 ISize.toInt32 ISize.toInt64 ISize.toInt8 ISize.toNatClampNeg ISize.xor IdId.run IdempotentOpIdentIffIff.elim Iff.intro InfinitelyUpwardEnumerableInhabitedInhabited.mk InjectiveIntInt.add Int.bdiv Int.bmod Int.cast Int.decEq Int.ediv Int.emod Int.fdiv Int.fmod Int.gcd Int.lcm Int.le Int.lt Int.mul Int.natAbs Int.neg Int.negOfNat Int.negSucc Int.not Int.ofNat Int.pow Int.repr Int.shiftRight Int.sign Int.sub Int.subNatNat Int.tdiv Int.tmod Int.toISize Int.toInt16 Int.toInt32 Int.toInt64 Int.toInt8 Int.toNat Int.toNat? Int16Int16.abs Int16.add Int16.complement Int16.decEq Int16.decLe Int16.decLt Int16.div Int16.land Int16.le Int16.lor Int16.lt Int16.maxValue Int16.minValue Int16.mod Int16.mul Int16.neg Int16.ofBitVec Int16.ofInt Int16.ofIntClamp Int16.ofIntLE Int16.ofNat Int16.ofUInt16 Int16.shiftLeft Int16.shiftRight Int16.size Int16.sub Int16.toBitVec Int16.toFloat Int16.toFloat32 Int16.toISize Int16.toInt Int16.toInt32 Int16.toInt64 Int16.toInt8 Int16.toNatClampNeg Int16.xor Int32Int32.abs Int32.add Int32.complement Int32.decEq Int32.decLe Int32.decLt Int32.div Int32.land Int32.le Int32.lor Int32.lt Int32.maxValue Int32.minValue Int32.mod Int32.mul Int32.neg Int32.ofBitVec Int32.ofInt Int32.ofIntClamp Int32.ofIntLE Int32.ofNat Int32.ofUInt32 Int32.shiftLeft Int32.shiftRight Int32.size Int32.sub Int32.toBitVec Int32.toFloat Int32.toFloat32 Int32.toISize Int32.toInt Int32.toInt16 Int32.toInt64 Int32.toInt8 Int32.toNatClampNeg Int32.xor Int64Int64.abs Int64.add Int64.complement Int64.decEq Int64.decLe Int64.decLt Int64.div Int64.land Int64.le Int64.lor Int64.lt Int64.maxValue Int64.minValue Int64.mod Int64.mul Int64.neg Int64.ofBitVec Int64.ofInt Int64.ofIntClamp Int64.ofIntLE Int64.ofNat Int64.ofUInt64 Int64.shiftLeft Int64.shiftRight Int64.size Int64.sub Int64.toBitVec Int64.toFloat Int64.toFloat32 Int64.toISize Int64.toInt Int64.toInt16 Int64.toInt32 Int64.toInt8 Int64.toNatClampNeg Int64.xor Int8Int8.abs Int8.add Int8.complement Int8.decEq Int8.decLe Int8.decLt Int8.div Int8.land Int8.le Int8.lor Int8.lt Int8.maxValue Int8.minValue Int8.mod Int8.mul Int8.neg Int8.ofBitVec Int8.ofInt Int8.ofIntClamp Int8.ofIntLE Int8.ofNat Int8.ofUInt8 Int8.shiftLeft Int8.shiftRight Int8.size Int8.sub Int8.toBitVec Int8.toFloat Int8.toFloat32 Int8.toISize Int8.toInt Int8.toInt16 Int8.toInt32 Int8.toInt64 Int8.toNatClampNeg Int8.xor IntCastIntCast.mk IntModuleIntervalInvariantInvariantIsAlwaysFiniteIsAlwaysFiniteIsCharPIsInfixIsPlausibleIndirectOutputIsPlausibleStepIsPrefixIsSuffixIterIterMIterStepIteratorIteratorIteratorIteratorAccessIteratorLoopiididid_mapidempotentidentidentKind- identifier
- identifier
idxidxOfidxOfidxOf?idxOf?ififfimpimpimplicitDefEqProofs- impredicative
- inaccessible
incincreaseByindindindindentDindexindex- index
- indexed family
inductSkipsinductSkipsinductStepsinductStepsinductioninductioninductionOninductionOninductionOninductive.autoPromoteIndices inductiveCheckResultingUniverseinferControlInfoEleminferControlInfoSeqinferInstanceinferInstanceAsinfer_instanceinflateinhabitedLeftinhabitedLeftinhabitedRightinhabitedRightinheritEnvinit(Lake command)injectioninjectionsinnerinnerinnerinnerinnerinnerinnerinnerinnerinnerinsertinsertinsertinsertinsertinsertinsertinsertinsertinsertinsertIdx!insertIdxinsertIdxinsertIdxIfInBoundsinsertIdxTRinsertIfNewinsertIfNewinsertIfNewinsertIfNewinsertIfNewinsertIfNewinsertManyinsertManyinsertManyinsertManyinsertManyinsertManyinsertManyinsertManyinsertManyinsertManyIfNewUnitinsertManyIfNewUnitinsertManyIfNewUnitinsertionSort- instance synthesis
instanceinstancesinstancesinstancesinstantiateintCastintCastintCast_negintCast_ofNatintMaxintMinintercalateintercalateintercalateTRinternalStateinternalStateinternalizeinternalizeinternalize_allinterpolatedStrKindinterpolatedStrLitKindintersperseintersperseTRintro(0) (1) (2)intros(0) (1)invImageinv_zeroiotaiotaisAbsoluteisAlphaisAlphanumisCancelledisCancelledisDefaultisDigitisDirisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmptyisEmscriptenisEqisEqSomeisEqvisEqvisExclusiveUnsafeisFiniteisFiniteisFiniteisGEisGTisInfisInfisInfisIntisLEisLTisLeftisLowerisLtisNaNisNaNisNaNisNatisNatisNatisNeisNilisNoneisOSXisOfKindisOkisPermisPowerOfTwoisPrefixOfisPrefixOfisPrefixOfisPrefixOf?isPureApp?isRelativeisResolvedisRightisSomeisSome_succ?isSublistisSuffixOfisSuffixOf?isTtyisTtyisUpperisValidisValidisValidCharisValidCharisValidCharNatisValidForSliceisValidForSliceisValidUTF8isWhitespaceisWindowsiseqvitititeriteriteriteriteriteriteriteriteriteriteriteriteriteriteriteriteriteriteriterFromIdxiterFromIdxMiterMiterMiterateiterateiunfoldriunfoldr_replace
J
joinjoinjoinjoinjoinSepjoinSuffixjoinTask
K
kkeepAlivekeepAlivekeyAtIdx!keyAtIdxkeyAtIdx?keyAtIdxDkeyskeyskeyskeyskeysArraykeysArraykeysArraykeysArraykeysIterkeysIterkeysIterkeysIterkillkindkleisliLeftkleisliRight
L
LAKE(environment variable)LAKE_ARTIFACT_CACHE(environment variable)LAKE_CACHE_ARTIFACT_ENDPOINT(environment variable)LAKE_CACHE_KEY(environment variable)LAKE_CACHE_REVISION_ENDPOINT(environment variable)LAKE_HOME(environment variable)LAKE_NO_CACHE(environment variable)LAKE_OVERRIDE_LEAN(environment variable)LELELE.mk LEAN(environment variable)LEAN_AR(environment variable)LEAN_CC(environment variable)LEAN_NUM_THREADS(environment variable)LEAN_SYSROOT(environment variable)LTLTLT.mk Lake.Backend Lake.Backend. c Lake.Backend. default Lake.Backend. llvm Lake.BuildType Lake.BuildType. debug Lake.BuildType. minSizeRel Lake.BuildType. relWithDebInfo Lake.BuildType. release Lake.Glob Lake.Glob. andSubmodules Lake.Glob. one Lake.Glob. submodules Lake.LeanExeConfig Lake.LeanExeConfig. mk Lake.LeanLibConfig Lake.LeanLibConfig. mk Lake.MonadLakeEnv Lake.MonadWorkspace Lake.MonadWorkspace. mk Lake.(0) (1)ScriptM Lake.findExternLib? Lake.findLeanExe? Lake.findLeanLib? Lake.findModule? Lake.findPackageByKey? Lake.findPackageByName? Lake.getAugmentedEnv Lake.getAugmentedLeanPath Lake.getAugmentedLeanSrcPath Lake.getElan? Lake.getElanHome? Lake.getElanInstall? Lake.getElanToolchain Lake.getEnvLeanPath Lake.getEnvLeanSrcPath Lake.getLake Lake.getLakeEnv Lake.getLakeHome Lake.getLakeInstall Lake.getLakeLibDir Lake.getLakeSrcDir Lake.getLean Lake.getLeanAr Lake.getLeanCc Lake.getLeanCc? Lake.getLeanIncludeDir Lake.getLeanInstall Lake.getLeanLibDir Lake.getLeanPath Lake.getLeanSrcDir Lake.getLeanSrcPath Lake.getLeanSysroot Lake.getLeanSystemLibDir Lake.getLeanc Lake.getNoCache Lake.getPkgUrlMap Lake.getRootPackage Lake.getTryCache LawfulApplicativeLawfulApplicative.mk LawfulBEqLawfulBEq.mk LawfulFunctorLawfulFunctor.mk LawfulGetElemLawfulGetElem.mk LawfulHashableLawfulHashable.mk LawfulIdentityLawfulIteratorLoopLawfulMonadLawfulMonad.mk' LawfulMonad.mk LawfulUpwardEnumerableLeadingIdentBehaviorLean.Elab. Command. Linter Lean.Elab. Command. Linter. mk Lean.Elab. Command. ModuleLinter Lean.Elab. Command. ModuleLinter. mk Lean.Elab. Command. PreStateFn Lean.Elab. Command. PrevStateFn Lean.Elab. Command. StatefulLinter Lean.Elab. Command. addLinter Lean.Elab. Command. addModuleLinter Lean.Elab. Command. registerStatefulLinter Lean.Elab. Do. CodeLiveness Lean.Elab. Do. CodeLiveness. alive Lean.Elab. Do. CodeLiveness. deadSemantically Lean.Elab. Do. CodeLiveness. deadSyntactically Lean.Elab. Do. ContInfo Lean.Elab. Do. ContInfo. mk Lean.Elab. Do. ContInfoRef. toContInfo Lean.Elab. Do. Context Lean.Elab. Do. Context. mk Lean.Elab. Do. ControlInfo Lean.Elab. Do. ControlInfo. alternative Lean.Elab. Do. ControlInfo. empty Lean.Elab. Do. ControlInfo. mk Lean.Elab. Do. ControlInfo. pure Lean.Elab. Do. ControlInfo. sequence Lean.Elab. Do. ControlInfoHandler Lean.Elab. Do. DoElab Lean.Elab. Do. DoElemCont Lean.Elab. Do. DoElemCont. continueWithUnit Lean.Elab. Do. DoElemCont. elabAsSyntacticallyDeadCode Lean.Elab. Do. DoElemCont. ensureHasTypeAt Lean.Elab. Do. DoElemCont. ensureUnit Lean.Elab. Do. DoElemCont. ensureUnitAt Lean.Elab. Do. DoElemCont. mk Lean.Elab. Do. DoElemCont. mkBindUnlessPure Lean.Elab. Do. DoElemCont. withDuplicableCont Lean.Elab. Do. DoElemContKind Lean.Elab. Do. DoElemContKind. duplicable Lean.Elab. Do. DoElemContKind. nonDuplicable Lean.Elab. Do. DoOps Lean.Elab. Do. DoOps. mk Lean.Elab. Do. DoOpsRef. toDoOps Lean.Elab. Do. EffectForwarder Lean.Elab. Do. EffectForwarder. lift Lean.Elab. Do. EffectForwarder. mk Lean.Elab. Do. EffectForwarder. ofCont Lean.Elab. Do. EffectForwarder. restoreCont Lean.Elab. Do. InferControlInfo. ofElem Lean.Elab. Do. InferControlInfo. ofLetOrReassign Lean.Elab. Do. InferControlInfo. ofLetOrReassignArrow Lean.Elab. Do. InferControlInfo. ofOptionSeq Lean.Elab. Do. InferControlInfo. ofSeq Lean.Elab. Do. MonadInfo Lean.Elab. Do. MonadInfo. mk Lean.Elab. Do. MutVar Lean.Elab. Do. MutVar. mk Lean.Elab. Do. declareMutVar Lean.Elab. Do. declareMutVars Lean.Elab. Do. elabDoElem Lean.Elab. Do. elabDoElems1 Lean.Elab. Do. elabDoSeq Lean.Elab. Do. enterLoopBody Lean.Elab. Do. getBreakCont Lean.Elab. Do. getContinueCont Lean.Elab. Do. getReturnCont Lean.Elab. Do. inferControlInfoElem Lean.Elab. Do. inferControlInfoSeq Lean.Elab. Do. mkBindApp Lean.Elab. Do. mkMonadApp Lean.Elab. Do. mkPUnitUnit Lean.Elab. Do. mkPureApp Lean.Elab. Do. throwUnlessMutVarDeclared Lean.Elab. Do. throwUnlessMutVarsDeclared Lean.Elab. registerDerivingHandler Lean.Grind. AddRightCancel Lean.Grind. AddRightCancel. mk Lean.Grind. CommRing Lean.Grind. CommRing. mk Lean.Grind. CommSemiring Lean.Grind. CommSemiring. mk Lean.Grind. Field Lean.Grind. Field. mk Lean.Grind. IntModule Lean.Grind. IntModule. mk Lean.Grind. IsCharP Lean.Grind. IsCharP. mk Lean.Grind. NatModule Lean.Grind. NatModule. mk Lean.Grind. NoNatZeroDivisors Lean.Grind. NoNatZeroDivisors. mk' Lean.Grind. NoNatZeroDivisors. mk Lean.Grind. OrderedAdd Lean.Grind. OrderedAdd. mk Lean.Grind. OrderedRing Lean.Grind. OrderedRing. mk Lean.Grind. Ring Lean.Grind. Ring. mk Lean.Grind. Semiring Lean.Grind. Semiring. mk Lean.LeanOption Lean.LeanOption. mk Lean.Linter. CodeQuality. Entry Lean.Linter. CodeQuality. Entry. mk Lean.Linter. CodeQuality. PackageCheck Lean.Linter. CodeQuality. PackageCheck. ofFn Lean.Linter. CodeQuality. PackageCheckContext Lean.Linter. CodeQuality. PackageCheckContext. mk Lean.Linter. CodeQuality. Source Lean.Linter. CodeQuality. Source. declaration Lean.Linter. CodeQuality. Source. module Lean.Linter. CodeQuality. Value Lean.Linter. CodeQuality. Value. dict Lean.Linter. CodeQuality. Value. scalar Lean.Linter. EnvLinter. EnvLinter Lean.Linter. EnvLinter. EnvLinter. mk Lean.Linter. addEnvLinterOption Lean.Linter. findCodeQualitySource Lean.Linter. findCodeQualitySource? Lean.Linter. findMatchingDecl? Lean.Linter. getLinterOptions Lean.Linter. getLinterValue Lean.Linter. logCodeQualityEntry Lean.Linter. logCodeQualityEntryIf Lean.Linter. logLint Lean.Linter. logLintIf Lean.Macro. Exception. unsupportedSyntax Lean.Macro. addMacroScope Lean.Macro. expandMacro? Lean.Macro. getCurrNamespace Lean.Macro. hasDecl Lean.Macro. resolveGlobalName Lean.Macro. resolveNamespace Lean.Macro. throwError Lean.Macro. throwErrorAt Lean.Macro. throwUnsupported Lean.Macro. trace Lean.Macro. withFreshMacroScope Lean.MacroM Lean.Meta. DSimp. Config Lean.Meta. DSimp. Config. mk Lean.Meta. Occurrences Lean.Meta. Occurrences. all Lean.Meta. Occurrences. neg Lean.Meta. Occurrences. pos Lean.Meta. Rewrite. Config Lean.Meta. Rewrite. Config. mk Lean.Meta. Rewrite. NewGoals Lean.Meta. Simp. Config Lean.Meta. Simp. Config. mk Lean.Meta. Simp. neutralConfig Lean.Meta. SimpExtension Lean.Meta. TransparencyMode Lean.Meta. TransparencyMode. all Lean.Meta. TransparencyMode. default Lean.Meta. TransparencyMode. implicit Lean.Meta. TransparencyMode. instances Lean.Meta. TransparencyMode. none Lean.Meta. TransparencyMode. reducible Lean.Meta. registerSimpAttr Lean.Order. CCPO Lean.Order. CCPO. mk Lean.Order. CompleteLattice Lean.Order. CompleteLattice. mk Lean.Order. CompleteLattice. ofProp Lean.Order. PartialOrder Lean.Order. PartialOrder. mk Lean.Order. PredTrans Lean.Order. PredTrans. Monotone Lean.Order. PredTrans. bind Lean.Order. PredTrans. mk Lean.Order. PredTrans. pure Lean.Order. PredTrans. pushArg Lean.Order. PredTrans. pushExceptT Lean.Order. PredTrans. pushOptionT Lean.Order. fix Lean.Order. fix_eq Lean.Order. lfp Lean.Order. lfp_fix Lean.Order. lfp_le_of_le_monotone Lean.Order. monotone Lean.Parser. LeadingIdentBehavior Lean.Parser. LeadingIdentBehavior. both Lean.Parser. LeadingIdentBehavior. default Lean.Parser. LeadingIdentBehavior. symbol Lean.PrettyPrinter. UnexpandM Lean.PrettyPrinter. Unexpander Lean.Quote Lean.Quote. mk Lean.SourceInfo Lean.SourceInfo. none Lean.SourceInfo. original Lean.SourceInfo. synthetic Lean.Syntax Lean.Syntax. CharLit Lean.Syntax. Command Lean.Syntax. HygieneInfo Lean.Syntax. Ident Lean.Syntax. Level Lean.Syntax. NameLit Lean.Syntax. NumLit Lean.Syntax. Prec Lean.Syntax. Preresolved Lean.Syntax. Preresolved. decl Lean.Syntax. Preresolved. namespace Lean.Syntax. Prio Lean.Syntax. ScientificLit Lean.Syntax. StrLit Lean.Syntax. TSepArray Lean.Syntax. TSepArray. elemsAndSeps Lean.Syntax. TSepArray. getElems Lean.Syntax. TSepArray. mk Lean.Syntax. TSepArray. ofElems Lean.Syntax. TSepArray. push Lean.Syntax. Tactic Lean.Syntax. Term Lean.Syntax. atom Lean.Syntax. getKind Lean.Syntax. ident Lean.Syntax. isOfKind Lean.Syntax. missing Lean.Syntax. mkApp Lean.Syntax. mkCApp Lean.Syntax. mkCharLit Lean.Syntax. mkLit Lean.Syntax. mkNameLit Lean.Syntax. mkNatLit Lean.Syntax. mkNumLit Lean.Syntax. mkScientificLit Lean.Syntax. mkStrLit Lean.Syntax. node Lean.Syntax. setKind Lean.SyntaxNodeKind Lean.SyntaxNodeKinds Lean.TSyntax Lean.TSyntax. getChar Lean.TSyntax. getHygieneInfo Lean.TSyntax. getId Lean.TSyntax. getName Lean.TSyntax. getNat Lean.TSyntax. getScientific Lean.TSyntax. getString Lean.TSyntax. mk Lean.TSyntaxArray Lean.TSyntaxArray. raw Lean.charLitKind Lean.choiceKind Lean.fieldIdxKind Lean.groupKind Lean.hygieneInfoKind Lean.identKind Lean.interpolatedStrKind Lean.interpolatedStrLitKind Lean.mkCIdent Lean.mkCIdentFrom Lean.mkCIdentFromRef Lean.mkGroupNode Lean.mkHole Lean.mkIdent Lean.mkIdentFrom Lean.mkIdentFromRef Lean.mkOptionalNode Lean.nameLitKind Lean.nullKind Lean.numLitKind Lean.scientificLitKind Lean.strLitKind Lean.withSetOptionIn LeanExeConfigLeanLibConfigLeanOptionLeast?LeftInverseLevelLexLinearlyUpwardEnumerableLinterListList.Cursor List.Cursor. at List.Cursor. begin List.Cursor. current List.Cursor. end List.Cursor. mk List.Cursor. pos List.Cursor. tail List.IsInfix List.IsPrefix List.IsSuffix List.Lex List.Lex. cons List.Lex. nil List.Lex. rel List.Mem List.Mem. head List.Mem. tail List.Nodup List.Pairwise List.Pairwise. cons List.Pairwise. nil List.Perm List.Perm. cons List.Perm. nil List.Perm. swap List.Perm. trans List.Sublist List.Sublist. cons List.Sublist. cons_cons List.Sublist. slnil List.all List.allM List.and List.any List.anyM List.append List.appendTR List.attach List.attachWith List.beq List.concat List.cons List.contains List.count List.countP List.drop List.dropLast List.dropLastTR List.dropWhile List.elem List.erase List.eraseDups List.eraseIdx List.eraseIdxTR List.eraseP List.erasePTR List.eraseReps List.eraseTR List.extract List.filter List.filterM List.filterMap List.filterMapM List.filterMapTR List.filterRevM List.filterTR List.finIdxOf? List.finRange List.find? List.findFinIdx? List.findIdx List.findIdx? List.findM? List.findSome? List.findSomeM? List.firstM List.flatMap List.flatMapM List.flatMapTR List.flatten List.flattenTR List.foldl List.foldlM List.foldlRecOn List.foldr List.foldrM List.foldrRecOn List.foldrTR List.forA List.forM List.get List.getD List.getLast List.getLast! List.getLast? List.getLastD List.groupByKey List.head List.head! List.head? List.headD List.idxOf List.idxOf? List.insert List.insertIdx List.insertIdxTR List.intercalate List.intercalateTR List.intersperse List.intersperseTR List.isEmpty List.isEqv List.isPerm List.isPrefixOf List.isPrefixOf? List.isSublist List.isSuffixOf List.isSuffixOf? List.iter List.iterM List.le List.leftpad List.leftpadTR List.length List.lengthTR List.lex List.lookup List.lt List.map List.mapA List.mapFinIdx List.mapFinIdxM List.mapIdx List.mapIdxM List.mapM List.mapM' List.mapMono List.mapMonoM List.mapTR List.max? List.merge List.mergeSort List.min? List.modify List.modifyHead List.modifyTR List.modifyTailIdx List.nil List.ofFn List.or List.partition List.partitionM List.partitionMap List.pmap List.range List.range' List.range'TR List.removeAll List.replace List.replaceTR List.replicate List.replicateTR List.reverse List.rightpad List.rotateLeft List.rotateRight List.set List.setTR List.singleton List.span List.splitAt List.splitBy List.sum List.tail List.tail! List.tail? List.tailD List.take List.takeTR List.takeWhile List.takeWhileTR List.toArray List.toArrayImpl List.toByteArray List.toFloatArray List.toString List.unattach List.unzip List.unzipTR List.zip List.zipIdx List.zipIdxTR List.zipWith List.zipWithAll List.zipWithTR landlandlandlandlandlandlandlandlandlandlandlandlastlastCaseslawfullazyPurelcmlcmleleleleleleleleleleleleleleleleleleleleOfOrdle_wplean(Lake command)lean_is_arraylean_is_stringlean_string_object(0) (1)lean_to_arraylean_to_stringleast?left(0) (1)leftleft_distribleftpadleftpadleftpadTRlegacylengthlengthlengthlengthlengthTRletlet reclet'letIletToHavelet_to_have- level
lex'lexlexlexlexLtlfplfp_fixlfp_le_of_le_monotonelhslia(0) (1)libNamelibPrefixOnWindowsliftliftliftliftliftliftliftliftliftliftliftliftliftOnliftOnliftOn₂liftWithliftWithliftWithPropertylift_letsliftedDoBlockResultTypeliftedStacklift₂linarithlineEqlineslineslint(Lake command)linter.all linter.coreInternal linter.extra linter.unnecessarySimpa listen- literal
- literal
localslocalslocklogloglog10log10log2log2log2log2log2log2log2log2log2logCodeQualityEntrylogCodeQualityEntryIflogLintlogLintIflookuplorlorlorlorlorlorlorlorlorlorlorlorlowerlowerlowerlowerlowerlowerltltltltltltltltltltltltltltltltltltltltOfOrd
M
MProdMProd.mk MacroMMaxMax.mk MaybeTaskMemMembershipMetadataMinMin.mk ModMod.mk ModeModelModelModuleLinterMonadMonad.mk MonadAsyncMonadAwaitMonadControlMonadControl.mk MonadControlTMonadControlT.mk MonadEvalMonadEval.mk MonadEvalTMonadEvalT.mk MonadExceptMonadExcept.mk MonadExcept.ofExcept MonadExcept.orElse MonadExcept.orelse' MonadExceptOfMonadExceptOf.mk MonadFinallyMonadFinally.mk MonadFunctorMonadFunctor.mk MonadFunctorTMonadFunctorT.mk MonadInfoMonadLakeEnvMonadLiftMonadLift.mk MonadLiftTMonadLiftT.mk MonadPrettyFormatMonadReaderMonadReader.mk MonadReaderOfMonadReaderOf.mk MonadStateMonadState.get MonadState.mk MonadState.modifyGet MonadStateOfMonadStateOf.mk MonadWithReaderMonadWithReader.mk MonadWithReaderOfMonadWithReaderOf.mk MonadWorkspaceMonotoneMonotonicMulMul.mk MutVarMutexm- main goal
mapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmapmap- map
- map
mapAmapAmapConstmapErrormapFinIdxmapFinIdxmapFinIdxMmapFinIdxMmapIdxmapIdxmapIdxMmapIdxMmapListmapM'mapM'mapMmapMmapMmapMmapMmapMonomapMonomapMonoMmapMonoMmapRevmapTRmapTaskmapTaskmapTaskmapTaskIOmapTasksmapTasksmapTasksmapWithPostconditionmapWithPostconditionmap_constmap_puremassumptionmatchmatchmax!maxmaxmaxmaxmaxmax?max?maxDmaxDischargeDepthmaxEntry!maxEntrymaxEntry?maxEntryDmaxHeartbeatsmaxKey!maxKeymaxKey?maxKeyDmaxOfLemaxSizemaxStepsmaxStepsmaxStepsmaxSuggestionsmaxValuemaxValuemaxValuemaxValuemaxValuemayThrowmbtcmcasesmclearmconstructormdupmemoizemergemergemergemergeSortmergeWithmetadatamexactmexfalsomexistsmframemhavemin!minminminminminmin?min?minDminEntry!minEntryminEntry?minEntryDminKey!minKeyminKey?minKeyDminOfLeminValueminValueminValueminValueminValuemintromixHashmk'mk'mk'mkmkmkmkmkmkmkmkmkmkmkmkmkmkAppmkBindAppmkBindAppmkBindUnlessPuremkCAppmkCIdentmkCIdentFrommkCIdentFromRefmkCharLitmkFilePathmkGroupNodemkHolemkIdentmkIdentFrommkIdentFromRefmkIteratormkLitmkMonadAppmkMonadAppmkNameLitmkNatLitmkNumLitmkOptionalNodemkPUnitUnitmkPureAppmkPureAppmkRefmkRefmkScientificLitmkSlicemkSlicemkSlicemkSlicemkSlicemkSlicemkSlicemkSlicemkSlicemkStdGenmkStrLitmleavemleftmodmodmodmodmodmodmodmodmodmodmodmodmodmodCoremodifiedmodifymodifymodifymodifymodifymodifymodifymodifymodifymodifymodifymodifymodifyGetmodifyGetmodifyGetmodifyGetmodifyGetmodifyGetmodifyGetmodifyGetThemodifyHeadmodifyMmodifyOpmodifyTRmodifyTailIdxmodifyThemodnmonadEvalmonadEvalmonadInfomonadLiftmonadLiftmonadMapmonadMapmonoMsNowmonoNanosNowmonotonempmpmpmpmprmprmpurempure_intromrefinemrename_imreplacemrightmsbmspecmspecializemspecialize_puremstartmstopmulmulmulmulmulmulmulmulmulmulmulmulmulmulmulmulmulmulmulRecmul_assocmul_commmul_inv_cancelmul_lt_mul_of_pos_leftmul_lt_mul_of_pos_rightmul_onemul_zeromutVarDefsmutVarsmvarsmvcgen
N
NameInfoNameLitNatNat.add Nat.all Nat.allM Nat.allTR Nat.any Nat.anyM Nat.anyTR Nat.beq Nat.bitwise Nat.ble Nat.blt Nat.caseStrongRecOn Nat.casesAuxOn Nat.cast Nat.decEq Nat.decLe Nat.decLt Nat.digitChar Nat.div Nat.div. inductionOn Nat.div2Induction Nat.fold Nat.foldM Nat.foldRev Nat.foldRevM Nat.foldTR Nat.forM Nat.forRevM Nat.gcd Nat.isPowerOfTwo Nat.isValidChar Nat.land Nat.lcm Nat.le Nat.le. refl Nat.le. step Nat.log2 Nat.lor Nat.lt Nat.max Nat.min Nat.mod Nat.mod. inductionOn Nat.modCore Nat.mul Nat.nextPowerOfTwo Nat.pow Nat.pred Nat.recAux Nat.repeat Nat.repeatTR Nat.repr Nat.shiftLeft Nat.shiftRight Nat.strongRecOn Nat.sub Nat.subDigitChar Nat.succ Nat.superDigitChar Nat.testBit Nat.toDigits Nat.toFloat Nat.toFloat32 Nat.toISize Nat.toInt16 Nat.toInt32 Nat.toInt64 Nat.toInt8 Nat.toSubDigits Nat.toSubscriptString Nat.toSuperDigits Nat.toSuperscriptString Nat.toUInt16 Nat.toUInt32 Nat.toUInt64 Nat.toUInt8 Nat.toUSize Nat.xor Nat.zero NatCastNatCast.mk NatModuleNatPowNatPow.mk NeZeroNeZero.mk NegNeg.mk NewGoalsNoNatZeroDivisorsNodupNonemptyNonempty.intro NotNot.elim NumLitnamenamenamenamenameLitKind- namespace
natAbsnatAddnatCastnatCastnativenativenativenativenativenativeFacetsnative_decidendrecndrecOnne_of_ltneedsnegnegnegnegnegnegnegnegnegnegnegnegnegnegnegnegnegOfNatneg_add_cancelneg_zsmulnestDneutralConfignew(Lake command)newnewnewnewnewnewnewGoalsnextnext ...=> ... next =>next!next!next'next'next'nextnextnextnextnextnextnextnextnext?next?nextAtIdx?nextAtIdx?nextPowerOfTwonextUntilnextWhilenextnnextnnextnnextnnilnoDelaynoDelaynoErrorsFoundnoFallthroughnoThrowno_nat_zero_divisorsnofunnomatchnonBacktrackablenorm_cast(0) (1)normalizenotnotnotnotnotMnotifyAllnotifyOnenpownsmulnsmulnsmul_eq_natCast_mulnullKindnumBitsnumLinksnumLitKindnumRegularExits
O
OccurrencesOfNatOfNat.mk OfScientificOfScientific.mk OptionOption.all Option.any Option.attach Option.attachWith Option.bind Option.bindM Option.choice Option.decidableEqNone Option.elim Option.elimM Option.filter Option.filterM Option.forM Option.format Option.get Option.get! Option.getD Option.getDM Option.getM Option.guard Option.isEqSome Option.isNone Option.isSome Option.join Option.lt Option.map Option.mapA Option.mapM Option.max Option.merge Option.min Option.none Option.or Option.orElse Option.pbind Option.pelim Option.pmap Option.repr Option.sequence Option.some Option.toArray Option.toList Option.tryCatch Option.unattach OptionTOptionT.bind OptionT.fail OptionT.lift OptionT.mk OptionT.orElse OptionT.pure OptionT.run OptionT.tryCatch OrOr.by_cases Or.by_cases' Or.inl Or.inr OrOpOrOp.mk OrdOrd.lex Ord.lex' Ord.mk Ord.on Ord.opposite Ord.toBEq Ord.toLE Ord.toLT OrderedAddOrderedRingOrderingOrdering.eq Ordering.gt Ordering.isEq Ordering.isGE Ordering.isGT Ordering.isLE Ordering.isLT Ordering.isNe Ordering.lt Ordering.swap Ordering.then OutputobtainoccsofArrayofArrayofArrayofArrayofAsyncTaskofBitVecofBitVecofBitVecofBitVecofBitVecofBitsofBitsofBoolofBoolListBEofBoolListLEofBufferofByteArrayofContofCopyofETaskofElemofElemsofExceptofExceptofExceptofExceptofExceptofFinofFinofFinofFinofFinofFnofFnofHandleofIOTaskofISizeofIntofIntofIntofIntofIntofIntofIntofIntofIntofInt16ofInt32ofInt64ofInt8ofIntClampofIntClampofIntClampofIntClampofIntClampofIntLEofIntLEofIntLEofIntLEofIntLEofLetOrReassignofLetOrReassignArrowofListofListofListofListofListofListofListofListofListofListofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNatofNat32ofNatClampofNatClampofNatClampofNatClampofNatClampofNatLTofNatLTofNatLTofNatLTofNatLTofNatLTofNat_eq_natCastofNat_ext_iffofNat_succofOptionSeqofPromise!ofPromiseofPropofPurePromiseofScientificofScientificofSeqofSliceofSliceFromofSliceToofSubarrayofTaskofTaskofTaskofUInt16ofUInt32ofUInt64ofUInt8ofUInt8ofUSizeof_eq_wpof_eq_wpof_run'_eq_wpof_run_eq_wpof_run_eq_wpof_run_eq_wpof_run_eq_wpof_wp_eqof_wp_run'_eqof_wp_run_eqof_wp_run_eqof_wp_run_eqof_wp_run_eqoffsetoffsetoffsetByoffsetCnstrsoffsetOfPosomegaononeone_mulone_zsmulopenoperationoperationoppositeopsoptParamoptionalorororororororElse'orElseorElseorElseorElseorElseorElseorElseorElseLazyorMorelse'origContotheroutoutoutoutoutoutoutParamoutputoverride list(Elan command)override set(Elan command)override unset(Elan command)
P
PEmptyPEmpty.elim PLiftPLift.up PProdPProd.mk PSigmaPSigma.mk PSumPSum.inhabitedLeft PSum.inhabitedRight PSum.inl PSum.inr PUnitPUnit.unit PackageCheckPackageCheckContextPairwisePartialOrderPermPlausibleIterStepPosPosPostCondPostShapePostconditionTPowPow.mk PreStateFnPrecPredTransPredTransPreresolvedPrevStateFnPrioPriorityProdProd.allI Prod.anyI Prod.foldI Prod.lexLt Prod.map Prod.mk Prod.swap ProductiveProductivePromisePropPropertyPropertyPurePure.mk pack(Lake command)packpack- parameter
parenparent- parser
partitionpartitionpartitionpartitionpartitionpartitionpartitionpartitionpartitionMpartitionMappathpathExistspathSeparatorpathSeparatorspatternpbindpbindpelim- placeholder term
pmappmappmappmap- polymorphism
poppopFrontpopWhilepos!pos!pospospospospospospos?pos?posGEposGTposOfpositionspowpowpowpowpowpowpowpow_succpow_zeropppp.deepTerms pp.deepTerms. threshold pp.fieldNotation pp.match pp.maxSteps pp.mvars pp.proofs pp.proofs. threshold precompileLibraryprecompileModulespredpredpred- predicative
prefixprefixJoinprettyprettyMprev!prev!prevprevprevprevprevprevprev?prev?prevnprevnprevnprevnprintprintlnprivateInPublicprojproj- proof state
proofsproofsInPublicpropertypropertypropext- proposition
- proposition
prunptrAddrUnsafeptrEqptrEqptrEqListpurepurepurepurepurepurepurepurepurepurepurepurepurepurepure_bindpure_le_wp_purepure_seqpushpushpushpushpushArgpushArgpushExceptpushExceptTpushNewlinepushOptionpushOptionTpushOutputpush_castpushnputputStrputStrputStrLnputStrLn
Q
QuotQuot.hrecOn Quot.ind Quot.lift Quot.liftOn Quot.mk Quot.rec Quot.recOn Quot.recOnSubsingleton Quot.sound QuoteQuotientQuotient.exact Quotient.hrecOn Quotient.ind Quotient.lift Quotient.liftOn Quotient.liftOn₂ Quotient.lift₂ Quotient.mk Quotient.mk' Quotient.rec Quotient.recOn Quotient.recOnSubsingleton Quotient.recOnSubsingleton₂ Quotient.sound qsortqsortOrd- quantification
- quantification
query(Lake command)quotequotequote
R
RandomGenRandomGen.mk RawRawRawRawRawRawRawRawRccRciRcoReaderMReaderTReaderT.adapt ReaderT.bind ReaderT.failure ReaderT.orElse ReaderT.pure ReaderT.read ReaderT.run RefRefReflBEqReflBEq.mk ReprRepr.addAppParen Repr.mk ReprAtomReprAtom.mk ResultRicRightInverseRiiRingRioRocRoiRoorraceraceraceraceraceraceAllraceAllraceAllraceAllrandrandBoolrandNatrange'range'range'TRrangerangerangerawrawrawEndPosrawEndPosrcasesreadreadreadreadreadreadreadreadBinFilereadBinToEndreadBinToEndIntoreadDirreadFilereadThereadToEndrealPathreasonreassignsrecrecrecAuxrecOnrecOnrecOnSubsingletonrecOnSubsingletonrecOnSubsingleton₂- recursor
recvrecvrecv?recvSelectorrecvSelectorrecvSelectorrecvSelectorrecvSelectorreduce- reduction
refinerefine'reflreflreflects_decideregisterDerivingHandlerregisterFnregisterSimpAttrregisterStatefulLinterrelrelrel_antisymmrel_reflrel_transrelaxedAutoImplicitremainingBytesremainingBytesremainingToStringremoveAllremoveDirremoveDirAllremoveFileremoveLeadingSpacesrenamerenamerename_i(0) (1)repairrepeat(0) (1) (2)repeat'repeatrepeatrepeat1'repeatTRreplacereplacereplacereplacereplaceTRreplicatereplicatereplicatereplicateTRreprreprreprreprreprreprreprArgreprPrecreprStrresetresetresolveresolveGlobalNameresolveNamespacerestorerestoreContrestoreMrestoreMresult!resultresult?resultDresultNameresultTypereturnBase?returnContreturnsEarlyreuseSubInstancesrevrevBytesrevCharsrevFind?revFind?revPositionsrevSplitreversereversereversereverseInductionrevertrewindrewrite(0) (1)rewriterfl(0) (1) (2)rfl'rflrflrhsright(0) (1)rightright_distribrightpadrightpadringrintrorootrootrootsrotateLeftrotateLeftrotateRightrotateRightrotate_leftrotate_rightroundroundrun(Elan command)run'run'run'run'runrunrunrunrunrunrunrunrunrunrunrunrunrunrunrunCatchrunESTrunInrunKrunKrunSTrun_tacrw(0) (1) (2)rw?rw_mod_castrwa
S
SMulSMul.mk SPredSTST.Ref ST.Ref. get ST.Ref. mk ST.Ref. modify ST.Ref. modifyGet ST.Ref. ptrEq ST.Ref. put ST.Ref. set ST.Ref. swap ST.Ref. take ST.Ref. toMonadStateOf ST.mkRef STWorldSTWorld.mk SValScientificLitScriptMSelectableSelectorSemiringSeqSeq.mk SeqLeftSeqLeft.mk SeqRightSeqRight.mk ServerSetoidSetoid.mk Setoid.refl Setoid.symm Setoid.trans ShiftLeftShiftLeft.mk ShiftRightShiftRight.mk ShrinkSigmaSigma.mk SignalSimpExtensionSizeOfSizeOf.mk SleepSliceSliceableSliceableSliceableSliceableSliceableSliceableSliceableSliceableSliceableSortSourceSourceInfoSpawnArgsSquashSquash.ind Squash.lift Squash.mk StateStateStateCpsTStateCpsT.lift StateCpsT.run StateCpsT.run' StateCpsT.runK StateMStateRefT'StateRefT'.get StateRefT'.lift StateRefT'.modifyGet StateRefT'.run StateRefT'.run' StateRefT'.set StateTStateT.bind StateT.failure StateT.get StateT.lift StateT.map StateT.modifyGet StateT.orElse StateT.pure StateT.run StateT.run' StateT.set StateTupleStatefulLinterStd.Associative Std.Associative. mk Std.Async. Async Std.Async. Async. block Std.Async. Async. concurrently Std.Async. Async. concurrentlyAll Std.Async. Async. ofAsyncTask Std.Async. Async. ofExcept Std.Async. Async. ofIOTask Std.Async. Async. ofPromise Std.Async. Async. ofPurePromise Std.Async. Async. ofTask Std.Async. Async. race Std.Async. Async. raceAll Std.Async. Async. toIO Std.Async. AsyncTask Std.Async. AsyncTask. bindIO Std.Async. AsyncTask. block Std.Async. AsyncTask. getState Std.Async. AsyncTask. map Std.Async. AsyncTask. mapTaskIO Std.Async. BaseAsync Std.Async. BaseAsync. asTask Std.Async. BaseAsync. concurrently Std.Async. BaseAsync. concurrentlyAll Std.Async. BaseAsync. ofExcept Std.Async. BaseAsync. ofTask Std.Async. BaseAsync. race Std.Async. BaseAsync. raceAll Std.Async. BaseAsync. toBaseIO Std.Async. BaseAsync. wait Std.Async. ContextAsync Std.Async. ContextAsync. async Std.Async. ContextAsync. awaitCancellation Std.Async. ContextAsync. background Std.Async. ContextAsync. cancel Std.Async. ContextAsync. concurrently Std.Async. ContextAsync. concurrentlyAll Std.Async. ContextAsync. disown Std.Async. ContextAsync. doneSelector Std.Async. ContextAsync. getCancellationReason Std.Async. ContextAsync. getContext Std.Async. ContextAsync. isCancelled Std.Async. ContextAsync. race Std.Async. ContextAsync. raceAll Std.Async. ContextAsync. run Std.Async. ContextAsync. runIn Std.Async. DNS. NameInfo Std.Async. DNS. NameInfo. mk Std.Async. DNS. getAddrInfo Std.Async. DNS. getNameInfo Std.Async. EAsync Std.Async. EAsync. asTask Std.Async. EAsync. block Std.Async. EAsync. concurrently Std.Async. EAsync. concurrentlyAll Std.Async. EAsync. ofETask Std.Async. EAsync. ofExcept Std.Async. EAsync. ofTask Std.Async. EAsync. race Std.Async. EAsync. raceAll Std.Async. EAsync. toEIO Std.Async. EAsync. wait Std.Async. ETask Std.Async. ETask. block Std.Async. ETask. getState Std.Async. ETask. ofPromise! Std.Async. IO. AsyncRead Std.Async. IO. AsyncRead. mk Std.Async. IO. AsyncStream Std.Async. IO. AsyncStream. mk Std.Async. IO. AsyncWrite Std.Async. IO. AsyncWrite. mk Std.Async. Interval Std.Async. Interval. mk Std.Async. Interval. reset Std.Async. Interval. stop Std.Async. Interval. tick Std.Async. MaybeTask Std.Async. MaybeTask. get Std.Async. MaybeTask. joinTask Std.Async. MaybeTask. map Std.Async. MaybeTask. ofTask Std.Async. MaybeTask. pure Std.Async. MaybeTask. toTask Std.Async. MonadAsync Std.Async. MonadAsync. mk Std.Async. MonadAwait Std.Async. MonadAwait. mk Std.Async. Selectable Std.Async. Selectable. case Std.Async. Selectable. combine Std.Async. Selectable. one Std.Async. Selectable. tryOne Std.Async. Selector Std.(0) (1)Async. Selector. cancelled Std.Async. Selector. mk Std.Async. Selector. sleep Std.Async. Signal Std.Async. Signal. Waiter Std.Async. Signal. Waiter. mk Std.(0) (1)Async. Signal. Waiter. selector Std.Async. Signal. Waiter. stop Std.Async. Signal. Waiter. wait Std.Async. Signal. sigabrt Std.Async. Signal. sigalrm Std.Async. Signal. sigchld Std.Async. Signal. sigcont Std.Async. Signal. sighup Std.Async. Signal. sigint Std.Async. Signal. sigio Std.Async. Signal. sigprof Std.Async. Signal. sigquit Std.Async. Signal. sigsys Std.Async. Signal. sigterm Std.Async. Signal. sigtrap Std.Async. Signal. sigtstp Std.Async. Signal. sigttin Std.Async. Signal. sigttou Std.Async. Signal. sigurg Std.Async. Signal. sigusr1 Std.Async. Signal. sigusr2 Std.Async. Signal. sigvtalrm Std.Async. Signal. sigwinch Std.Async. Signal. sigxcpu Std.Async. Signal. sigxfsz Std.Async. Sleep Std.Async. Sleep. mk Std.Async. Sleep. reset Std.Async. Sleep. selector Std.Async. Sleep. stop Std.Async. Sleep. wait Std.Async. TCP. Socket. Client Std.Async. TCP. Socket. Client. bind Std.Async. TCP. Socket. Client. connect Std.Async. TCP. Socket. Client. getPeerName Std.Async. TCP. Socket. Client. getSockName Std.Async. TCP. Socket. Client. keepAlive Std.Async. TCP. Socket. Client. mk Std.Async. TCP. Socket. Client. noDelay Std.Async. TCP. Socket. Client. recv? Std.Async. TCP. Socket. Client. recvSelector Std.Async. TCP. Socket. Client. send Std.Async. TCP. Socket. Client. sendAll Std.Async. TCP. Socket. Client. shutdown Std.Async. TCP. Socket. Server Std.Async. TCP. Socket. Server. accept Std.Async. TCP. Socket. Server. acceptSelector Std.Async. TCP. Socket. Server. bind Std.Async. TCP. Socket. Server. getSockName Std.Async. TCP. Socket. Server. keepAlive Std.Async. TCP. Socket. Server. listen Std.Async. TCP. Socket. Server. mk Std.Async. TCP. Socket. Server. noDelay Std.Async. TCP. Socket. Server. tryAccept Std.Async. UDP. Membership Std.Async. UDP. Membership. enterGroup Std.Async. UDP. Membership. leaveGroup Std.Async. UDP. Socket. bind Std.Async. UDP. Socket. connect Std.Async. UDP. Socket. getPeerName Std.Async. UDP. Socket. getSockName Std.Async. UDP. Socket. mk Std.Async. UDP. Socket. recv Std.Async. UDP. Socket. recvSelector Std.Async. UDP. Socket. send Std.Async. UDP. Socket. sendAll Std.Async. UDP. Socket. setBroadcast Std.Async. UDP. Socket. setMembership Std.Async. UDP. Socket. setMulticastInterface Std.Async. UDP. Socket. setMulticastLoop Std.Async. UDP. Socket. setMulticastTTL Std.Async. UDP. Socket. setTTL Std.Async. Waiter Std.Async. Waiter. checkFinished Std.Async. Waiter. race Std.Async. Waiter. withPromise Std.Async. background Std.Async. sleep Std.AtomicT Std.Broadcast. Receiver. recvSelector Std.CancellationContext Std.CancellationContext. State Std.CancellationContext. State. mk Std.CancellationContext. cancel Std.CancellationContext. done Std.(0) (1)CancellationContext. doneSelector Std.CancellationContext. fork Std.CancellationContext. getCancellationReason Std.CancellationContext. isCancelled Std.CancellationContext. new Std.CancellationReason Std.CancellationReason. cancel Std.CancellationReason. custom Std.CancellationReason. deadline Std.CancellationReason. shutdown Std.CancellationToken Std.CancellationToken. Consumer Std.CancellationToken. Consumer. normal Std.CancellationToken. Consumer. select Std.CancellationToken. State Std.CancellationToken. State. mk Std.CancellationToken. mk Std.CancellationToken. selector Std.Channel Std.Channel. Sync Std.Channel. forAsync Std.Channel. new Std.Channel. recv Std.Channel. recvSelector Std.Channel. send Std.Channel. sync Std.CloseableChannel Std.CloseableChannel. new Std.CloseableChannel. recvSelector Std.Commutative Std.Commutative. mk Std.Condvar Std.Condvar. new Std.Condvar. notifyAll Std.Condvar. notifyOne Std.Condvar. wait Std.Condvar. waitUntil Std.DHashMap Std.DHashMap. Equiv Std.DHashMap. Equiv. mk Std.DHashMap. Raw Std.DHashMap. Raw. WF Std.DHashMap. Raw. WF. alter₀ Std.DHashMap. Raw. WF. constAlter₀ Std.DHashMap. Raw. WF. constGetThenInsertIfNew?₀ Std.DHashMap. Raw. WF. constModify₀ Std.DHashMap. Raw. WF. containsThenInsertIfNew₀ Std.DHashMap. Raw. WF. containsThenInsert₀ Std.DHashMap. Raw. WF. emptyWithCapacity₀ Std.DHashMap. Raw. WF. erase₀ Std.DHashMap. Raw. WF. filter₀ Std.DHashMap. Raw. WF. getThenInsertIfNew?₀ Std.DHashMap. Raw. WF. insertIfNew₀ Std.DHashMap. Raw. WF. insert₀ Std.DHashMap. Raw. WF. inter₀ Std.DHashMap. Raw. WF. modify₀ Std.DHashMap. Raw. WF. wf Std.DHashMap. Raw. mk Std.DHashMap. alter Std.DHashMap. contains Std.DHashMap. containsThenInsert Std.DHashMap. containsThenInsertIfNew Std.DHashMap. emptyWithCapacity Std.DHashMap. erase Std.DHashMap. filter Std.DHashMap. filterMap Std.DHashMap. fold Std.DHashMap. foldM Std.DHashMap. forIn Std.DHashMap. forM Std.DHashMap. get Std.DHashMap. get! Std.DHashMap. get? Std.DHashMap. getD Std.DHashMap. getKey Std.DHashMap. getKey! Std.DHashMap. getKey? Std.DHashMap. getKeyD Std.DHashMap. getThenInsertIfNew? Std.DHashMap. insert Std.DHashMap. insertIfNew Std.DHashMap. insertMany Std.DHashMap. isEmpty Std.DHashMap. iter Std.DHashMap. keys Std.DHashMap. keysArray Std.DHashMap. keysIter Std.DHashMap. map Std.DHashMap. modify Std.DHashMap. ofList Std.DHashMap. partition Std.DHashMap. size Std.DHashMap. toArray Std.DHashMap. toList Std.DHashMap. union Std.DHashMap. values Std.DHashMap. valuesArray Std.DHashMap. valuesIter Std.DTreeMap Std.DTreeMap. Raw Std.DTreeMap. Raw. WF Std.DTreeMap. Raw. WF. mk Std.DTreeMap. Raw. mk Std.DTreeMap. alter Std.DTreeMap. contains Std.DTreeMap. containsThenInsert Std.DTreeMap. containsThenInsertIfNew Std.DTreeMap. empty Std.DTreeMap. erase Std.DTreeMap. filter Std.DTreeMap. filterMap Std.DTreeMap. foldl Std.DTreeMap. foldlM Std.DTreeMap. forIn Std.DTreeMap. forM Std.DTreeMap. get Std.DTreeMap. get! Std.DTreeMap. get? Std.DTreeMap. getD Std.DTreeMap. getKey Std.DTreeMap. getKey! Std.DTreeMap. getKey? Std.DTreeMap. getKeyD Std.DTreeMap. getThenInsertIfNew? Std.DTreeMap. insert Std.DTreeMap. insertIfNew Std.DTreeMap. insertMany Std.DTreeMap. isEmpty Std.DTreeMap. iter Std.DTreeMap. keys Std.DTreeMap. keysArray Std.DTreeMap. keysIter Std.DTreeMap. map Std.DTreeMap. modify Std.DTreeMap. ofList Std.DTreeMap. partition Std.DTreeMap. size Std.DTreeMap. toArray Std.DTreeMap. toList Std.DTreeMap. values Std.DTreeMap. valuesArray Std.DTreeMap. valuesIter Std.Do. Assertion Std.Do. EStateM. of_wp_run_eq Std.Do. Except. of_wp_eq Std.Do. ExceptConds Std.Do. Id. of_wp_run_eq Std.Do. Invariant Std.Do. Invariant. withEarlyReturn Std.Do. PostCond Std.Do. PostCond. and Std.Do. PostCond. entails Std.Do. PostCond. imp Std.Do. PostCond. mayThrow Std.Do. PostCond. noThrow Std.Do. PostShape Std.Do. PostShape. arg Std.Do. PostShape. args Std.Do. PostShape. except Std.Do. PostShape. pure Std.Do. PredTrans Std.Do. PredTrans. Conjunctive Std.Do. PredTrans. Monotonic Std.Do. PredTrans. bind Std.Do. PredTrans. mk Std.Do. PredTrans. pure Std.Do. PredTrans. pushArg Std.Do. PredTrans. pushExcept Std.Do. PredTrans. pushOption Std.Do. ReaderM. of_wp_run_eq Std.Do. SPred Std.Do. SPred. and Std.Do. SPred. bientails Std.Do. SPred. conjunction Std.Do. SPred. entails Std.Do. SPred. exists Std.Do. SPred. forall Std.Do. SPred. iff Std.Do. SPred. imp Std.Do. SPred. not Std.Do. SPred. or Std.Do. SPred. pure Std.Do. SVal Std.Do. SVal. StateTuple Std.Do. SVal. curry Std.Do. SVal. getThe Std.Do. SVal. uncurry Std.Do. StateM. of_wp_run'_eq Std.Do. StateM. of_wp_run_eq Std.Do. Triple Std.Do. Triple. and Std.Do. Triple. mp Std.Do. WP Std.Do. WP. mk Std.Do. WPMonad Std.Do. WPMonad. mk Std.ExtDHashMap Std.ExtDHashMap. alter Std.ExtDHashMap. contains Std.ExtDHashMap. containsThenInsert Std.ExtDHashMap. containsThenInsertIfNew Std.ExtDHashMap. emptyWithCapacity Std.ExtDHashMap. erase Std.ExtDHashMap. filter Std.ExtDHashMap. filterMap Std.ExtDHashMap. get Std.ExtDHashMap. get! Std.ExtDHashMap. get? Std.ExtDHashMap. getD Std.ExtDHashMap. getKey Std.ExtDHashMap. getKey! Std.ExtDHashMap. getKey? Std.ExtDHashMap. getKeyD Std.ExtDHashMap. getThenInsertIfNew? Std.ExtDHashMap. insert Std.ExtDHashMap. insertIfNew Std.ExtDHashMap. insertMany Std.ExtDHashMap. isEmpty Std.ExtDHashMap. map Std.ExtDHashMap. modify Std.ExtDHashMap. ofList Std.ExtDHashMap. size Std.ExtHashMap Std.ExtHashMap. alter Std.ExtHashMap. contains Std.ExtHashMap. containsThenInsert Std.ExtHashMap. containsThenInsertIfNew Std.ExtHashMap. emptyWithCapacity Std.ExtHashMap. erase Std.ExtHashMap. filter Std.ExtHashMap. filterMap Std.ExtHashMap. get Std.ExtHashMap. get! Std.ExtHashMap. get? Std.ExtHashMap. getD Std.ExtHashMap. getKey Std.ExtHashMap. getKey! Std.ExtHashMap. getKey? Std.ExtHashMap. getKeyD Std.ExtHashMap. getThenInsertIfNew? Std.ExtHashMap. insert Std.ExtHashMap. insertIfNew Std.ExtHashMap. insertMany Std.ExtHashMap. insertManyIfNewUnit Std.ExtHashMap. isEmpty Std.ExtHashMap. map Std.ExtHashMap. modify Std.ExtHashMap. ofList Std.ExtHashMap. size Std.ExtHashMap. unitOfArray Std.ExtHashMap. unitOfList Std.ExtHashSet Std.ExtHashSet. contains Std.ExtHashSet. containsThenInsert Std.ExtHashSet. emptyWithCapacity Std.ExtHashSet. erase Std.ExtHashSet. filter Std.ExtHashSet. get Std.ExtHashSet. get! Std.ExtHashSet. get? Std.ExtHashSet. getD Std.ExtHashSet. insert Std.ExtHashSet. insertMany Std.ExtHashSet. isEmpty Std.ExtHashSet. mk Std.ExtHashSet. ofArray Std.ExtHashSet. ofList Std.ExtHashSet. size Std.Format Std.Format. FlattenBehavior Std.Format. FlattenBehavior. allOrNone Std.Format. FlattenBehavior. fill Std.Format. MonadPrettyFormat Std.Format. MonadPrettyFormat. mk Std.Format. align Std.Format. append Std.Format. bracket Std.Format. bracketFill Std.Format. defIndent Std.Format. defWidth Std.Format. fill Std.Format. group Std.Format. indentD Std.Format. isEmpty Std.Format. isNil Std.Format. join Std.Format. joinSep Std.Format. joinSuffix Std.Format. line Std.Format. nest Std.Format. nestD Std.Format. nil Std.Format. paren Std.Format. prefixJoin Std.Format. pretty Std.Format. prettyM Std.Format. sbracket Std.Format. tag Std.Format. text Std.HashMap Std.HashMap. Equiv Std.HashMap. Equiv. mk Std.HashMap. Raw Std.HashMap. Raw. WF Std.HashMap. Raw. WF. mk Std.HashMap. Raw. mk Std.HashMap. alter Std.HashMap. contains Std.HashMap. containsThenInsert Std.HashMap. containsThenInsertIfNew Std.HashMap. emptyWithCapacity Std.HashMap. erase Std.HashMap. filter Std.HashMap. filterMap Std.HashMap. fold Std.HashMap. foldM Std.HashMap. forIn Std.HashMap. forM Std.HashMap. get Std.HashMap. get! Std.HashMap. get? Std.HashMap. getD Std.HashMap. getKey Std.HashMap. getKey! Std.HashMap. getKey? Std.HashMap. getKeyD Std.HashMap. getThenInsertIfNew? Std.HashMap. insert Std.HashMap. insertIfNew Std.HashMap. insertMany Std.HashMap. insertManyIfNewUnit Std.HashMap. isEmpty Std.HashMap. iter Std.HashMap. keys Std.HashMap. keysArray Std.HashMap. keysIter Std.HashMap. map Std.HashMap. modify Std.HashMap. ofList Std.HashMap. partition Std.HashMap. size Std.HashMap. toArray Std.HashMap. toList Std.HashMap. union Std.HashMap. unitOfArray Std.HashMap. unitOfList Std.HashMap. values Std.HashMap. valuesArray Std.HashMap. valuesIter Std.HashSet Std.HashSet. Equiv Std.HashSet. Equiv. mk Std.HashSet. Raw Std.HashSet. Raw. WF Std.HashSet. Raw. WF. mk Std.HashSet. Raw. mk Std.HashSet. all Std.HashSet. any Std.HashSet. contains Std.HashSet. containsThenInsert Std.HashSet. emptyWithCapacity Std.HashSet. erase Std.HashSet. filter Std.HashSet. fold Std.HashSet. foldM Std.HashSet. forIn Std.HashSet. forM Std.HashSet. get Std.HashSet. get! Std.HashSet. get? Std.HashSet. getD Std.HashSet. insert Std.HashSet. insertMany Std.HashSet. isEmpty Std.HashSet. iter Std.HashSet. mk Std.HashSet. ofArray Std.HashSet. ofList Std.HashSet. partition Std.HashSet. size Std.HashSet. toArray Std.HashSet. toList Std.HashSet. union Std.IdempotentOp Std.IdempotentOp. mk Std.Iter Std.Iter. Equiv Std.Iter. IsPlausibleIndirectOutput Std.Iter. IsPlausibleIndirectOutput. direct Std.Iter. IsPlausibleIndirectOutput. indirect Std.Iter. Step Std.Iter. all Std.Iter. allM Std.Iter. any Std.Iter. anyM Std.Iter. atIdx? Std.Iter. atIdxSlow? Std.Iter. attachWith Std.Iter. drop Std.Iter. dropWhile Std.Iter. empty Std.Iter. ensureTermination Std.Iter. filter Std.Iter. filterM Std.Iter. filterMap Std.Iter. filterMapM Std.Iter. filterMapWithPostcondition Std.Iter. filterWithPostcondition Std.Iter. find? Std.Iter. findM? Std.Iter. findSome? Std.Iter. findSomeM? Std.Iter. finitelyManySkips Std.Iter. finitelyManySteps Std.Iter. flatMap Std.Iter. flatMapAfter Std.Iter. flatMapAfterM Std.Iter. flatMapM Std.Iter. fold Std.Iter. foldM Std.Iter. inductSkips Std.Iter. inductSteps Std.Iter. length Std.Iter. map Std.Iter. mapM Std.Iter. mapWithPostcondition Std.Iter. mk Std.Iter. repeat Std.Iter. step Std.Iter. stepSize Std.Iter. take Std.Iter. takeWhile Std.Iter. toArray Std.Iter. toIterM Std.Iter. toList Std.Iter. toListRev Std.Iter. toTake Std.Iter. uLift Std.Iter. zip Std.IterM Std.IterM. Equiv Std.IterM. Step Std.IterM. TerminationMeasures. Finite Std.IterM. TerminationMeasures. Finite. mk Std.IterM. TerminationMeasures. Productive Std.IterM. TerminationMeasures. Productive. mk Std.IterM. all Std.IterM. allM Std.IterM. any Std.IterM. anyM Std.IterM. atIdx? Std.IterM. attachWith Std.IterM. drain Std.IterM. drop Std.IterM. dropWhile Std.IterM. dropWhileM Std.IterM. dropWhileWithPostcondition Std.IterM. empty Std.IterM. ensureTermination Std.IterM. filter Std.IterM. filterM Std.IterM. filterMap Std.IterM. filterMapM Std.IterM. filterMapWithPostcondition Std.IterM. filterWithPostcondition Std.IterM. find? Std.IterM. findM? Std.IterM. findSome? Std.IterM. findSomeM? Std.IterM. finitelyManySkips Std.IterM. finitelyManySteps Std.IterM. flatMap Std.IterM. flatMapAfter Std.IterM. flatMapAfterM Std.IterM. flatMapM Std.IterM. fold Std.IterM. foldM Std.IterM. inductSkips Std.IterM. inductSteps Std.IterM. length Std.IterM. map Std.IterM. mapM Std.IterM. mapWithPostcondition Std.IterM. mk Std.IterM. mk Std.IterM. nextAtIdx? Std.IterM. step Std.IterM. stepAsHetT Std.IterM. stepSize Std.IterM. take Std.IterM. takeWhile Std.IterM. takeWhileM Std.IterM. takeWhileWithPostcondition Std.IterM. toArray Std.IterM. toIter Std.IterM. toList Std.IterM. toListRev Std.IterM. toTake Std.IterM. uLift Std.IterM. zip Std.IterStep Std.IterStep. done Std.IterStep. skip Std.IterStep. yield Std.Iterator Std.Iterator. mk Std.IteratorAccess Std.IteratorAccess. mk Std.IteratorLoop Std.IteratorLoop. defaultImplementation Std.IteratorLoop. mk Std.Iterators. Finite Std.Iterators. Finite. mk Std.Iterators. HetT Std.Iterators. HetT. bind Std.Iterators. HetT. lift Std.Iterators. HetT. map Std.Iterators. HetT. mk Std.Iterators. HetT. pbind Std.Iterators. HetT. pmap Std.Iterators. HetT. prun Std.Iterators. HetT. pure Std.Iterators. PostconditionT Std.Iterators. PostconditionT. lift Std.Iterators. PostconditionT. liftWithProperty Std.Iterators. PostconditionT. mk Std.Iterators. PostconditionT. run Std.Iterators. Productive Std.Iterators. Productive. mk Std.LawfulIdentity Std.LawfulIdentity. mk Std.LawfulIteratorLoop Std.LawfulIteratorLoop. mk Std.Mutex Std.Mutex. atomically Std.Mutex. atomicallyOnce Std.Mutex. new Std.Notify. selector Std.PRange. InfinitelyUpwardEnumerable Std.PRange. InfinitelyUpwardEnumerable. mk Std.PRange. LawfulUpwardEnumerable Std.PRange. LawfulUpwardEnumerable. mk Std.PRange. Least? Std.PRange. Least?. mk Std.PRange. LinearlyUpwardEnumerable Std.PRange. LinearlyUpwardEnumerable. mk Std.PRange. UpwardEnumerable Std.PRange. UpwardEnumerable. LE Std.PRange. UpwardEnumerable. LT Std.PRange. UpwardEnumerable. mk Std.PlausibleIterStep Std.PlausibleIterStep. done Std.PlausibleIterStep. skip Std.PlausibleIterStep. yield Std.Rcc Std.Rcc. Sliceable Std.Rcc. Sliceable. mk Std.Rcc. isEmpty Std.Rcc. iter Std.Rcc. mk Std.Rcc. size Std.Rcc. toArray Std.Rcc. toList Std.Rci Std.Rci. Sliceable Std.Rci. Sliceable. mk Std.Rci. isEmpty Std.Rci. iter Std.Rci. mk Std.Rci. size Std.Rci. toArray Std.Rci. toList Std.Rco Std.Rco. Sliceable Std.Rco. Sliceable. mk Std.Rco. isEmpty Std.Rco. iter Std.Rco. mk Std.Rco. size Std.Rco. toArray Std.Rco. toList Std.Ric Std.Ric. Sliceable Std.Ric. Sliceable. mk Std.Ric. isEmpty Std.Ric. iter Std.Ric. mk Std.Ric. size Std.Ric. toArray Std.Ric. toList Std.Rii Std.Rii. Sliceable Std.Rii. Sliceable. mk Std.Rii. isEmpty Std.Rii. iter Std.Rii. mk Std.Rii. size Std.Rii. toArray Std.Rii. toList Std.Rio Std.Rio. Sliceable Std.Rio. Sliceable. mk Std.Rio. isEmpty Std.Rio. iter Std.Rio. mk Std.Rio. size Std.Rio. toArray Std.Rio. toList Std.Roc Std.Roc. Sliceable Std.Roc. Sliceable. mk Std.Roc. isEmpty Std.Roc. iter Std.Roc. mk Std.Roc. size Std.Roc. toArray Std.Roc. toList Std.Roi Std.Roi. Sliceable Std.Roi. Sliceable. mk Std.Roi. isEmpty Std.Roi. iter Std.Roi. mk Std.Roi. size Std.Roi. toArray Std.Roi. toList Std.Roo Std.Roo. Sliceable Std.Roo. Sliceable. mk Std.Roo. isEmpty Std.Roo. iter Std.Roo. mk Std.Roo. size Std.Roo. toArray Std.Roo. toList Std.Rxc. HasSize Std.Rxc. HasSize. mk Std.Rxc. IsAlwaysFinite Std.Rxc. IsAlwaysFinite. mk Std.Rxi. HasSize Std.Rxi. HasSize. mk Std.Rxi. IsAlwaysFinite Std.Rxi. IsAlwaysFinite. mk Std.Shrink Std.Shrink. deflate Std.Shrink. inflate Std.StreamMap. selector Std.ToFormat Std.ToFormat. mk Std.TreeMap Std.TreeMap. Raw Std.TreeMap. Raw. WF Std.TreeMap. Raw. WF. mk Std.TreeMap. Raw. mk Std.TreeMap. all Std.TreeMap. alter Std.TreeMap. any Std.TreeMap. contains Std.TreeMap. containsThenInsert Std.TreeMap. containsThenInsertIfNew Std.TreeMap. empty Std.TreeMap. entryAtIdx Std.TreeMap. entryAtIdx! Std.TreeMap. entryAtIdx? Std.TreeMap. entryAtIdxD Std.TreeMap. erase Std.TreeMap. eraseMany Std.TreeMap. filter Std.TreeMap. filterMap Std.TreeMap. foldl Std.TreeMap. foldlM Std.TreeMap. foldr Std.TreeMap. foldrM Std.TreeMap. forIn Std.TreeMap. forM Std.TreeMap. get Std.TreeMap. get! Std.TreeMap. get? Std.TreeMap. getD Std.TreeMap. getEntryGE Std.TreeMap. getEntryGE! Std.TreeMap. getEntryGE? Std.TreeMap. getEntryGED Std.TreeMap. getEntryGT Std.TreeMap. getEntryGT! Std.TreeMap. getEntryGT? Std.TreeMap. getEntryGTD Std.TreeMap. getEntryLE Std.TreeMap. getEntryLE! Std.TreeMap. getEntryLE? Std.TreeMap. getEntryLED Std.TreeMap. getEntryLT Std.TreeMap. getEntryLT! Std.TreeMap. getEntryLT? Std.TreeMap. getEntryLTD Std.TreeMap. getKey Std.TreeMap. getKey! Std.TreeMap. getKey? Std.TreeMap. getKeyD Std.TreeMap. getKeyGE Std.TreeMap. getKeyGE! Std.TreeMap. getKeyGE? Std.TreeMap. getKeyGED Std.TreeMap. getKeyGT Std.TreeMap. getKeyGT! Std.TreeMap. getKeyGT? Std.TreeMap. getKeyGTD Std.TreeMap. getKeyLE Std.TreeMap. getKeyLE! Std.TreeMap. getKeyLE? Std.TreeMap. getKeyLED Std.TreeMap. getKeyLT Std.TreeMap. getKeyLT! Std.TreeMap. getKeyLT? Std.TreeMap. getKeyLTD Std.TreeMap. getThenInsertIfNew? Std.TreeMap. insert Std.TreeMap. insertIfNew Std.TreeMap. insertMany Std.TreeMap. insertManyIfNewUnit Std.TreeMap. isEmpty Std.TreeMap. iter Std.TreeMap. keyAtIdx Std.TreeMap. keyAtIdx! Std.TreeMap. keyAtIdx? Std.TreeMap. keyAtIdxD Std.TreeMap. keys Std.TreeMap. keysArray Std.TreeMap. keysIter Std.TreeMap. map Std.TreeMap. maxEntry Std.TreeMap. maxEntry! Std.TreeMap. maxEntry? Std.TreeMap. maxEntryD Std.TreeMap. maxKey Std.TreeMap. maxKey! Std.TreeMap. maxKey? Std.TreeMap. maxKeyD Std.TreeMap. mergeWith Std.TreeMap. minEntry Std.TreeMap. minEntry! Std.TreeMap. minEntry? Std.TreeMap. minEntryD Std.TreeMap. minKey Std.TreeMap. minKey! Std.TreeMap. minKey? Std.TreeMap. minKeyD Std.TreeMap. modify Std.TreeMap. ofArray Std.TreeMap. ofList Std.TreeMap. partition Std.TreeMap. size Std.TreeMap. toArray Std.TreeMap. toList Std.TreeMap. unitOfArray Std.TreeMap. unitOfList Std.TreeMap. values Std.TreeMap. valuesArray Std.TreeMap. valuesIter Std.TreeSet Std.TreeSet. Raw Std.TreeSet. Raw. WF Std.TreeSet. Raw. WF. mk Std.TreeSet. Raw. mk Std.TreeSet. all Std.TreeSet. any Std.TreeSet. atIdx Std.TreeSet. atIdx! Std.TreeSet. atIdx? Std.TreeSet. atIdxD Std.TreeSet. contains Std.TreeSet. containsThenInsert Std.TreeSet. empty Std.TreeSet. erase Std.TreeSet. eraseMany Std.TreeSet. filter Std.TreeSet. foldl Std.TreeSet. foldlM Std.TreeSet. foldr Std.TreeSet. foldrM Std.TreeSet. forIn Std.TreeSet. forM Std.TreeSet. get Std.TreeSet. get! Std.TreeSet. get? Std.TreeSet. getD Std.TreeSet. getGE Std.TreeSet. getGE! Std.TreeSet. getGE? Std.TreeSet. getGED Std.TreeSet. getGT Std.TreeSet. getGT! Std.TreeSet. getGT? Std.TreeSet. getGTD Std.TreeSet. getLE Std.TreeSet. getLE! Std.TreeSet. getLE? Std.TreeSet. getLED Std.TreeSet. getLT Std.TreeSet. getLT! Std.TreeSet. getLT? Std.TreeSet. getLTD Std.TreeSet. insert Std.TreeSet. insertMany Std.TreeSet. isEmpty Std.TreeSet. iter Std.TreeSet. max Std.TreeSet. max! Std.TreeSet. max? Std.TreeSet. maxD Std.TreeSet. merge Std.TreeSet. min Std.TreeSet. min! Std.TreeSet. min? Std.TreeSet. minD Std.TreeSet. ofArray Std.TreeSet. ofList Std.TreeSet. partition Std.TreeSet. size Std.TreeSet. toArray Std.TreeSet. toList Std.WP. Assertion Std.WP. Assertion. mk Std.WP. EStateM. of_run_eq_wp Std.WP. Except. of_eq_wp Std.WP. Id. of_run_eq_wp Std.WP. Invariant Std.WP. Invariant. withEarlyReturnNewDo Std.WP. Option. of_eq_wp Std.WP. ReaderM. of_run_eq_wp Std.WP. StateM. of_run'_eq_wp Std.WP. StateM. of_run_eq_wp Std.WP. Triple Std.WP. Triple. and Std.WP. Triple. intro Std.WP. Triple. mp Std.WP. WP Std.WP. WP. mk Std.WP. WP. wp Std.WP. WPConjunctive Std.WP. WPConjunctive. mk Std.WP. WPMonad Std.WP. WPMonad. mk StdGenStdioStdioConfigStepStepStrLitStreamStringString.Legacy. Iterator String.Legacy. Iterator. atEnd String.Legacy. Iterator. curr String.Legacy. Iterator. curr' String.Legacy. Iterator. extract String.Legacy. Iterator. find String.Legacy. Iterator. foldUntil String.Legacy. Iterator. forward String.Legacy. Iterator. hasNext String.Legacy. Iterator. hasPrev String.Legacy. Iterator. mk String.Legacy. Iterator. next String.Legacy. Iterator. next' String.Legacy. Iterator. nextn String.Legacy. Iterator. pos String.Legacy. Iterator. prev String.Legacy. Iterator. prevn String.Legacy. Iterator. remainingBytes String.Legacy. Iterator. remainingToString String.Legacy. Iterator. setCurr String.Legacy. Iterator. toEnd String.Legacy. Iterator. toString String.Legacy. iter String.Legacy. mkIterator String.Pos String.Pos. Raw String.Pos. Raw. atEnd String.Pos. Raw. byteDistance String.Pos. Raw. dec String.Pos. Raw. decreaseBy String.Pos. Raw. extract String.Pos. Raw. get String.Pos. Raw. get! String.Pos. Raw. get' String.Pos. Raw. get? String.Pos. Raw. inc String.Pos. Raw. increaseBy String.Pos. Raw. isValid String.Pos. Raw. isValidForSlice String.Pos. Raw. min String.Pos. Raw. mk String.Pos. Raw. modify String.Pos. Raw. next String.Pos. Raw. next' String.Pos. Raw. nextUntil String.Pos. Raw. nextWhile String.Pos. Raw. offsetBy String.Pos. Raw. offsetOfPos String.Pos. Raw. prev String.Pos. Raw. set String.Pos. Raw. substrEq String.Pos. Raw. unoffsetBy String.Pos. byte String.Pos. cast String.Pos. get String.Pos. get! String.Pos. get? String.Pos. mk String.Pos. modify String.Pos. next String.Pos. next! String.Pos. next? String.Pos. ofCopy String.Pos. prev String.Pos. prev! String.Pos. prev? String.Pos. set String.Pos. toModifyOfLE String.Pos. toSetOfLE String.Pos. toSlice String.Slice String.Slice. Pattern. BackwardPattern String.Slice. Pattern. BackwardPattern. mk String.Slice. Pattern. ForwardPattern String.Slice. Pattern. ForwardPattern. mk String.Slice. Pattern. ToBackwardSearcher String.Slice. Pattern. ToBackwardSearcher. mk String.Slice. Pattern. ToForwardSearcher String.Slice. Pattern. ToForwardSearcher. mk String.Slice. Pos String.Slice. Pos. byte String.Slice. Pos. cast String.Slice. Pos. copy String.Slice. Pos. get String.Slice. Pos. get! String.Slice. Pos. get? String.Slice. Pos. mk String.Slice. Pos. next String.Slice. Pos. next! String.Slice. Pos. next? String.Slice. Pos. nextn String.Slice. Pos. ofSlice String.Slice. Pos. ofSliceFrom String.Slice. Pos. ofSliceTo String.Slice. Pos. prev String.Slice. Pos. prev! String.Slice. Pos. prev? String.Slice. Pos. prevn String.Slice. Pos. str String.Slice. all String.Slice. back String.Slice. back? String.Slice. beq String.Slice. bytes String.Slice. chars String.Slice. contains String.Slice. copy String.Slice. drop String.Slice. dropEnd String.Slice. dropEndWhile String.Slice. dropPrefix String.Slice. dropPrefix? String.Slice. dropSuffix String.Slice. dropSuffix? String.Slice. dropWhile String.Slice. endPos String.Slice. endsWith String.Slice. eqIgnoreAsciiCase String.Slice. find? String.Slice. foldl String.Slice. foldr String.Slice. front String.Slice. front? String.Slice. getUTF8Byte String.Slice. getUTF8Byte! String.Slice. isEmpty String.Slice. isNat String.Slice. lines String.Slice. mk String.Slice. pos String.Slice. pos! String.Slice. pos? String.Slice. posGE String.Slice. posGT String.Slice. positions String.Slice. rawEndPos String.Slice. revBytes String.Slice. revChars String.Slice. revFind? String.Slice. revPositions String.Slice. revSplit String.Slice. slice String.Slice. slice! String.Slice. sliceFrom String.Slice. sliceTo String.Slice. split String.Slice. splitInclusive String.Slice. startPos String.Slice. startsWith String.Slice. take String.Slice. takeEnd String.Slice. takeEndWhile String.Slice. takeWhile String.Slice. toNat! String.Slice. toNat? String.Slice. trimAscii String.Slice. trimAsciiEnd String.Slice. trimAsciiStart String.Slice. utf8ByteSize String.all String.any String.append String.back String.capitalize String.contains String.crlfToLf String.decEq String.decapitalize String.drop String.dropEnd String.dropEndWhile String.dropPrefix String.dropPrefix? String.dropSuffix String.dropSuffix? String.dropWhile String.endPos String.endsWith String.extract String.(0) (1)find String.firstDiffPos String.foldl String.foldr String.fromUTF8 String.fromUTF8! String.fromUTF8? String.front String.getUTF8Byte String.hash String.intercalate String.isEmpty String.isInt String.isNat String.isPrefixOf String.join String.le String.length String.map String.ofByteArray String.ofList String.pos String.pos! String.pos? String.push String.pushn String.quote String.rawEndPos String.removeLeadingSpaces String.replace String.revFind? String.singleton String.sliceFrom String.sliceTo String.splitOn String.splitToList String.startPos String.startsWith String.take String.takeEnd String.takeEndWhile String.takeWhile String.toFormat String.toInt! String.toInt? String.(0) (1)toList String.toLower String.toName String.toNat! String.toNat? String.toRawSubstring String.toRawSubstring' String.toSlice String.toUTF8 String.toUpper String.trimAscii String.trimAsciiEnd String.trimAsciiStart String.utf8ByteSize String.utf8EncodeChar SubSub.mk SubarraySubarray.all Subarray.allM Subarray.any Subarray.anyM Subarray.array Subarray.drop Subarray.empty Subarray.findRev? Subarray.findRevM? Subarray.findSomeRevM? Subarray.foldr Subarray.foldrM Subarray.forIn Subarray.forM Subarray.forRevM Subarray.get Subarray.get! Subarray.getD Subarray.popFront Subarray.split Subarray.start Subarray.start_le_stop Subarray.stop Subarray.stop_le_array_size Subarray.take SublistSubsingletonSubsingleton.elim Subsingleton.helim Subsingleton.intro Substring.Raw Substring.Raw. all Substring.Raw. any Substring.Raw. atEnd Substring.Raw. beq Substring.Raw. bsize Substring.Raw. commonPrefix Substring.Raw. commonSuffix Substring.Raw. contains Substring.Raw. drop Substring.Raw. dropPrefix? Substring.Raw. dropRight Substring.Raw. dropRightWhile Substring.Raw. dropSuffix? Substring.Raw. dropWhile Substring.Raw. extract Substring.Raw. foldl Substring.Raw. foldr Substring.Raw. front Substring.Raw. get Substring.Raw. isEmpty Substring.Raw. isNat Substring.Raw. mk Substring.Raw. next Substring.Raw. nextn Substring.Raw. posOf Substring.Raw. prev Substring.Raw. prevn Substring.Raw. repair Substring.Raw. sameAs Substring.Raw. splitOn Substring.Raw. take Substring.Raw. takeRight Substring.Raw. takeRightWhile Substring.Raw. takeWhile Substring.Raw. toLegacyIterator Substring.Raw. toName Substring.Raw. toNat? Substring.Raw. toString Substring.Raw. trim Substring.Raw. trimLeft Substring.Raw. trimRight SubtypeSubtype.mk SumSum.elim Sum.getLeft Sum.getLeft? Sum.getRight Sum.getRight? Sum.inhabitedLeft Sum.inhabitedRight Sum.inl Sum.inr Sum.isLeft Sum.isRight Sum.map Sum.swap SurjectiveSyncSyntaxSyntaxNodeKindSyntaxNodeKindsSystem.FilePath System.FilePath. addExtension System.FilePath. components System.FilePath. exeExtension System.FilePath. extSeparator System.FilePath. extension System.FilePath. fileName System.FilePath. fileStem System.FilePath. isAbsolute System.FilePath. isDir System.FilePath. isRelative System.FilePath. join System.FilePath. metadata System.FilePath. mk System.FilePath. normalize System.FilePath. parent System.FilePath. pathExists System.FilePath. pathSeparator System.FilePath. pathSeparators System.FilePath. readDir System.FilePath. symlinkMetadata System.FilePath. walkDir System.FilePath. withExtension System.FilePath. withFileName System.Platform. isEmscripten System.Platform. isOSX System.Platform. isWindows System.Platform. numBits System.Platform. target System.mkFilePath ssaddOverflowsameAssamply(Lake command)savesbracketscaleBscaleBscientificLitKindscript doc(Lake command)script list(Lake command)script run(Lake command)sdivselectorselectorselectorselectorselectorselectorself uninstall(Elan command)self update(Elan command)semiOutParamsendsendsendsendAllsendAllseqseqLeftseqLeft_eqseqRightseqRightseqRight_eqseq_assocseq_puresequencesequenceserve(Lake command)serviceset!set!setsetsetsetsetsetsetsetsetsetsetsetAccessRightssetBroadcastsetCurrsetCurrentDirsetIfInBoundssetKindsetMembershipsetMulticastInterfacesetMulticastLoopsetMulticastTTLsetRandSeedsetStderrsetStdinsetStdoutsetTRsetTTLsetWidth'setWidthset_configset_option(0) (1)setsidshake(Lake command)shiftConcatshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftshiftLeftRecshiftLeftZeroExtendshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshiftRightshowshow(Elan command)show_assertedshow_casesshow_eqcsshow_falseshow_goalsshow_local_thmsshow_stateshow_term(0) (1)show_trueshrinkshutdownsignsignExtendsimp(0) (1) (2)simp!simp?simp?!simp_allsimp_all!simp_all?simp_all?!simp_all_arithsimp_all_arith!simp_arithsimp_arith!simp_matchsimp_wfsimpasimpa!simpa?simpa?!simprocssinsinsinglePasssingletonsingletonsingletonsinhsinhsizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizesizeOfskip(0) (1) (2)skipskipAssignedInstancesskipPrefix?skipPrefixOfNonempty?skipSuffix?skipSuffixOfNonempty?slesleepsleepsleepsleepslice!sliceslicesliceFromsliceFromsliceTosliceTosltsmallsmodsmtSDivsmtUDivsmulsndsndsndsndsndsolvesolve_by_elimsorry(0) (1)soundsoundsourcespanspawnspawnspecializesplitsplitsplitsplitsplitsplitAtsplitBysplitInclusivesplitMonadApp?splitOnsplitOnsplitToListsqrtsqrtsqrtsrcDirsrcSearchPathsremsshiftRight'sshiftRightsshiftRightRecssubOverflowstMstMstartstartstartInclusivestartInclusive_le_endExclusivestartPosstartPosstartPosstartTagstart_le_stopstartsWithstartsWithstartsWithstatestatestdNextstdRangestdSplitstderrstderrstderrstdinstdinstdoutstdoutstdoutstepstepstepstepAsHetTstepSizestepSizestopstopstopstopstopstopstopstopPosstop_le_array_sizestrstrstrstrLitKindstrongRecOnsubsubsubsubsubsubsubsubsubsubsubsubsubsubsubsubsubsubsubDigitCharsubNatsubNatNatsub_eq_add_negsubstsubstsubstsubst_eqssubst_varssubstrEqsuccsucc?succMany?succMany?_add_onesuccMany?_zerosuccRecsuccRecOnsufficessuffixsuggestionssuggestionssumsumsuperDigitCharsupportInterpreterswapswapswapswapswapswapAt!swapAtswapIfInBoundssym =>symlinkMetadatasymmsymmsymmsymmsymm_saturatesyncsynthInstance.maxHeartbeats synthInstance.maxSize - synthesis
T
TSepArrayTSyntaxTSyntaxArrayTacticTaskTask.Priority Task.Priority. dedicated Task.Priority. default Task.Priority. max Task.bind Task.get Task.map Task.mapList Task.pure Task.spawn TaskStateTermThunkThunk.bind Thunk.get Thunk.map Thunk.mk Thunk.pure ToBackwardSearcherToFormatToForwardSearcherTransTrans.mk TransparencyModeTreeMapTreeSetTripleTripleTrueTrue.intro Typetactictactic =>tactic'tactic.customEliminators tactic.hygienic tactic.(0) (1)simp. trace tactic.skipAssignedInstances tail!tailtailtail?tailDtaketaketaketaketaketaketaketaketaketakeEndtakeEndtakeEndWhiletakeEndWhiletakeRighttakeRightWhiletakeStdintakeTRtakeWhiletakeWhiletakeWhiletakeWhiletakeWhiletakeWhiletakeWhiletakeWhileMtakeWhileTRtakeWhileWithPostconditiontantantanhtanhtargettdiv- term
test(Lake command)testtestBitthenthresholdthresholdthrowthrowthrowthrowErrorthrowErrorAtthrowThethrowUnlessMutVarDeclaredthrowUnlessMutVarsDeclaredthrowUnsupportedticktmodtoAddtoAddCommGrouptoAddCommMonoidtoApplicativetoApplicativetoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArraytoArrayImpltoBEqtoBaseIOtoBaseIOtoBindtoBitVectoBitVectoBitVectoBitVectoBitVectoBitVectoBitVectoBitVectoBitVectoBitVectoBitstoBitstoBitstoBitstoBooltoByteArraytoByteArraytoByteArraytoByteSlicetoCommRingtoCompleteLatticetoContInfotoDigitstoDivtoDoOpstoEIOtoEIOtoEIOtoEndtoEndtoFintoFintoFintoFintoFintoFintoFloattoFloattoFloattoFloattoFloattoFloattoFloattoFloattoFloattoFloattoFloattoFloattoFloat32toFloat32toFloat32toFloat32toFloat32toFloat32toFloat32toFloat32toFloat32toFloat32toFloat32toFloat32toFloatArraytoFormattoFunctortoGetElemtoHandleTypetoHextoIO'toIOtoIOtoIOtoISizetoISizetoISizetoISizetoISizetoISizetoISizetoISizetoISizetoISizetoISizetoIdentitytoInt!toInttoInttoInttoInttoInttoInttoInttoInt16toInt16toInt16toInt16toInt16toInt16toInt16toInt16toInt16toInt16toInt16toInt32toInt32toInt32toInt32toInt32toInt32toInt32toInt32toInt32toInt32toInt32toInt64toInt64toInt64toInt64toInt64toInt64toInt64toInt64toInt64toInt64toInt64toInt8toInt8toInt8toInt8toInt8toInt8toInt8toInt8toInt8toInt8toInt8toInt?toInvtoItertoIterMtoLEtoLTtoLawfulApplicativetoLawfulFunctortoLawfulLeftIdentitytoLawfulMonadtoLawfulMonadtoLawfulRightIdentitytoLeanConfigtoLeanConfigtoLegacyIteratortoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListtoListAppendtoListRevtoListRevtoListRevtoLowertoLowertoModeltoModeltoModifyOfLEtoMonadStateOftoMultoNametoNametoNat!toNat!toNattoNattoNattoNattoNattoNattoNattoNattoNattoNattoNat?toNat?toNat?toNat?toNatClampNegtoNatClampNegtoNatClampNegtoNatClampNegtoNatClampNegtoNegtoOptiontoOrderedAddtoPartialEquivBEqtoPartialOrdertoPartialOrdertoPuretoRawSubstring'toRawSubstringtoReflBEqtoReflBEqtoRingtoSearchertoSearchertoSemiringtoSemiringtoSeqtoSeqLefttoSeqRighttoSetOfLEtoSlicetoSlicetoStdioConfigtoStringtoStringtoStringtoStringtoStringtoStringtoStringtoStringtoSubtoSubDigitstoSubarraytoSubscriptStringtoSuperDigitstoSuperscriptStringtoTaketoTaketoTasktoUInt16toUInt16toUInt16toUInt16toUInt16toUInt16toUInt16toUInt16toUInt16toUInt16toUInt32toUInt32toUInt32toUInt32toUInt32toUInt32toUInt32toUInt32toUInt32toUInt32toUInt64toUInt64toUInt64toUInt64toUInt64toUInt64toUInt64toUInt64toUInt64toUInt64toUInt64BE!toUInt64LE!toUInt8toUInt8toUInt8toUInt8toUInt8toUInt8toUInt8toUInt8toUInt8toUInt8toUInt8toUSizetoUSizetoUSizetoUSizetoUSizetoUSizetoUSizetoUSizetoUSizetoUSizetoUTF8toUppertoUppertoVectortoWPtokentokenstoolchain gc(Elan command)toolchain install(Elan command)toolchain link(Elan command)toolchain list(Elan command)toolchain uninstall(Elan command)topLevelModuletracetracetracetrace.Elab. definition. wf trace.Meta. Tactic. simp. discharge trace.Meta. Tactic. simp. rewrite trace.compiler. ir. result trace.grind. ac trace.grind. ac. assert trace.grind. ac. basis trace.grind. ac. internalize trace.grind. ematch. instance trace.grind. hom trace.grind. hom. pred trace.grind. split trace_state(0) (1)transtranstranstranstranstranstrans_monotonetranslate-config(Lake command)transparencytrimtrimAsciitrimAsciitrimAsciiEndtrimAsciiEndtrimAsciiStarttrimAsciiStarttrimLefttrimRighttrivialtruncatetruncatetry(0) (1) (2)tryAccepttryCatchtryCatchtryCatchtryCatchtryCatchtryCatchtryCatchtryCatchThetryFinally'tryFntryLocktryOnetryWaittwoPow- type constructor
typetypetype_eq_of_heq
U
UInt16UInt16.add UInt16.complement UInt16.decEq UInt16.decLe UInt16.decLt UInt16.div UInt16.land UInt16.le UInt16.log2 UInt16.lor UInt16.lt UInt16.mod UInt16.mul UInt16.neg UInt16.ofBitVec UInt16.ofFin UInt16.ofNat UInt16.ofNatClamp UInt16.ofNatLT UInt16.shiftLeft UInt16.shiftRight UInt16.size UInt16.sub UInt16.toFin UInt16.toFloat UInt16.toFloat32 UInt16.toInt16 UInt16.toNat UInt16.toUInt32 UInt16.toUInt64 UInt16.toUInt8 UInt16.toUSize UInt16.xor UInt32UInt32.add UInt32.complement UInt32.decEq UInt32.decLe UInt32.decLt UInt32.div UInt32.isValidChar UInt32.land UInt32.le UInt32.log2 UInt32.lor UInt32.lt UInt32.mod UInt32.mul UInt32.neg UInt32.ofBitVec UInt32.ofFin UInt32.ofNat UInt32.ofNatClamp UInt32.ofNatLT UInt32.shiftLeft UInt32.shiftRight UInt32.size UInt32.sub UInt32.toFin UInt32.toFloat UInt32.toFloat32 UInt32.toInt32 UInt32.toNat UInt32.toUInt16 UInt32.toUInt64 UInt32.toUInt8 UInt32.toUSize UInt32.xor UInt64UInt64.add UInt64.complement UInt64.decEq UInt64.decLe UInt64.decLt UInt64.div UInt64.land UInt64.le UInt64.log2 UInt64.lor UInt64.lt UInt64.mod UInt64.mul UInt64.neg UInt64.ofBitVec UInt64.ofFin UInt64.ofNat UInt64.ofNatClamp UInt64.ofNatLT UInt64.shiftLeft UInt64.shiftRight UInt64.size UInt64.sub UInt64.toFin UInt64.toFloat UInt64.toFloat32 UInt64.toInt64 UInt64.toNat UInt64.toUInt16 UInt64.toUInt32 UInt64.toUInt8 UInt64.toUSize UInt64.xor UInt8UInt8.add UInt8.complement UInt8.decEq UInt8.decLe UInt8.decLt UInt8.div UInt8.land UInt8.le UInt8.log2 UInt8.lor UInt8.lt UInt8.mod UInt8.mul UInt8.neg UInt8.ofBitVec UInt8.ofFin UInt8.ofNat UInt8.ofNatClamp UInt8.ofNatLT UInt8.shiftLeft UInt8.shiftRight UInt8.size UInt8.sub UInt8.toFin UInt8.toFloat UInt8.toFloat32 UInt8.toInt8 UInt8.toNat UInt8.toUInt16 UInt8.toUInt32 UInt8.toUInt64 UInt8.toUSize UInt8.xor ULiftULift.up USizeUSize.add USize.complement USize.decEq USize.decLe USize.decLt USize.div USize.land USize.le USize.log2 USize.lor USize.lt USize.mod USize.mul USize.neg USize.ofBitVec USize.ofFin USize.ofNat USize.ofNat32 USize.ofNatClamp USize.ofNatLT USize.repr USize.shiftLeft USize.shiftRight USize.size USize.sub USize.toFin USize.toFloat USize.toFloat32 USize.toISize USize.toNat USize.toUInt16 USize.toUInt32 USize.toUInt64 USize.toUInt8 USize.xor UnexpandMUnexpanderUnitUnit.unit UnpackedFloatUpwardEnumerableuuLiftuLiftuaddOverflowudivugetugetuleultumodunattachunattachunattachuncurryuncurryunfold(0) (1)unfoldPartialAppunfoldPartialAppunhygienicunionunionunionunitunitOfArrayunitOfArrayunitOfArrayunitOfListunitOfListunitOfList- universe
- universe polymorphism
unlockunnecessarySimpaunoffsetByunpack(Lake command)unpackunpackunregisterFnunsafeBaseIOunsafeCastunsafeEIOunsafeIOunsupportedSyntaxunzipunzipunzipTRupdate(Lake command)upload(Lake command)upperupperupperupperupperupperuseuseruserErrorusetusetushiftRightushiftRightRecusizeusizeusubOverflowutf8ByteSizeutf8ByteSizeutf8Decode?utf8DecodeCharutf8DecodeChar?utf8EncodeCharutf8Size
V
ValuevvalvalvalvalidvalidvalidvaluevaluevaluevaluesvaluesvaluesvaluesvaluesArrayvaluesArrayvaluesArrayvaluesArrayvaluesItervaluesItervaluesItervaluesItervcgen
W
WFWFWFWFWFWFWPWPWPConjunctiveWPMonadWPMonadWaiterWaiterWellFoundedWellFounded.fix WellFounded.intro WellFoundedRelationWellFoundedRelation.mk waitwaitwaitwaitwaitwaitwaitwaitAnywaitUntilwalkDirwarnwarnExponentswarningwfwfwfwfwfParamwhich(Elan command)whnfwithDuplicableContwithEarlyReturnwithEarlyReturnNewDowithExtensionwithFilewithFileNamewithFreshMacroScopewithIsolatedStreamswithPositionwithPositionAfterLinebreakwithPromisewithReaderwithReaderwithSetOptionInwithStderrwithStdinwithStdoutwithTempDirwithTempFilewithTheReaderwith_reducible(0) (1)with_reducible_and_instances(0) (1)with_unfolding_all(0) (1)with_unfolding_nonewithoutPositionwpwpwpTranswp_bindwp_meet_wp_lewp_purewp_trans_monotonewrapwritewritewritewritewriteAllwriteBinFilewriteFile
X
XorOpXorOp.mk xorxorxorxorxorxorxorxorxorxorxorxorxorxorxor