git: 65781edef5d9 - main - math/lean4: Update to 4.22.0

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Wen Heping <wen_at_FreeBSD.org>
Date: Fri, 22 Aug 2025 02:53:06 UTC
The branch main has been updated by wen:

URL: https://cgit.FreeBSD.org/ports/commit/?id=65781edef5d9a9526707fcf4d6be747b5791e510

commit 65781edef5d9a9526707fcf4d6be747b5791e510
Author:     Wen Heping <wen@FreeBSD.org>
AuthorDate: 2025-08-22 02:47:34 +0000
Commit:     Wen Heping <wen@FreeBSD.org>
CommitDate: 2025-08-22 02:52:50 +0000

    math/lean4: Update to 4.22.0
    
    PR:             288987
    Approved by:    yuri@(maintainer)
---
 math/lean4/Makefile  |    3 +-
 math/lean4/distinfo  |    6 +-
 math/lean4/pkg-plist | 1527 ++++++++++++++++++++++++++++++++++++++++++++++++--
 3 files changed, 1475 insertions(+), 61 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index acc607f13634..8ac3190497f2 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,7 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.20.1
-PORTREVISION=	1
+DISTVERSION=	4.22.0
 CATEGORIES=	math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment
 
 MAINTAINER=	yuri@FreeBSD.org
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index 7a3ac889cce7..55b80a8bdc7c 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1749107862
-SHA256 (leanprover-lean4-v4.20.1_GH0.tar.gz) = 85b482da3748c404760a7492c331e5b6c74701d7913087b5da3616c5d949980f
-SIZE (leanprover-lean4-v4.20.1_GH0.tar.gz) = 40325710
+TIMESTAMP = 1755740882
+SHA256 (leanprover-lean4-v4.22.0_GH0.tar.gz) = 625aa7b9916b0dd9dd5c0a0f9b76d4921cc837528e799bd9ced8c6685c27651b
+SIZE (leanprover-lean4-v4.22.0_GH0.tar.gz) = 38212555
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 17ff0331ad17..a2d59c60ce54 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -8,1210 +8,1962 @@ include/lean/lean_gmp.h
 include/lean/lean_libuv.h
 include/lean/version.h
 lib/lean/Init.ilean
+lib/lean/Init.ir
 lib/lean/Init.olean
 lib/lean/Init.olean.private
 lib/lean/Init.olean.server
 lib/lean/Init/BinderNameHint.ilean
+lib/lean/Init/BinderNameHint.ir
 lib/lean/Init/BinderNameHint.olean
 lib/lean/Init/BinderNameHint.olean.private
 lib/lean/Init/BinderNameHint.olean.server
 lib/lean/Init/BinderPredicates.ilean
+lib/lean/Init/BinderPredicates.ir
 lib/lean/Init/BinderPredicates.olean
 lib/lean/Init/BinderPredicates.olean.private
 lib/lean/Init/BinderPredicates.olean.server
 lib/lean/Init/ByCases.ilean
+lib/lean/Init/ByCases.ir
 lib/lean/Init/ByCases.olean
 lib/lean/Init/ByCases.olean.private
 lib/lean/Init/ByCases.olean.server
 lib/lean/Init/Classical.ilean
+lib/lean/Init/Classical.ir
 lib/lean/Init/Classical.olean
 lib/lean/Init/Classical.olean.private
 lib/lean/Init/Classical.olean.server
 lib/lean/Init/Coe.ilean
+lib/lean/Init/Coe.ir
 lib/lean/Init/Coe.olean
 lib/lean/Init/Coe.olean.private
 lib/lean/Init/Coe.olean.server
 lib/lean/Init/Control.ilean
+lib/lean/Init/Control.ir
 lib/lean/Init/Control.olean
 lib/lean/Init/Control.olean.private
 lib/lean/Init/Control.olean.server
 lib/lean/Init/Control/Basic.ilean
+lib/lean/Init/Control/Basic.ir
 lib/lean/Init/Control/Basic.olean
 lib/lean/Init/Control/Basic.olean.private
 lib/lean/Init/Control/Basic.olean.server
 lib/lean/Init/Control/EState.ilean
+lib/lean/Init/Control/EState.ir
 lib/lean/Init/Control/EState.olean
 lib/lean/Init/Control/EState.olean.private
 lib/lean/Init/Control/EState.olean.server
 lib/lean/Init/Control/Except.ilean
+lib/lean/Init/Control/Except.ir
 lib/lean/Init/Control/Except.olean
 lib/lean/Init/Control/Except.olean.private
 lib/lean/Init/Control/Except.olean.server
 lib/lean/Init/Control/ExceptCps.ilean
+lib/lean/Init/Control/ExceptCps.ir
 lib/lean/Init/Control/ExceptCps.olean
 lib/lean/Init/Control/ExceptCps.olean.private
 lib/lean/Init/Control/ExceptCps.olean.server
 lib/lean/Init/Control/Id.ilean
+lib/lean/Init/Control/Id.ir
 lib/lean/Init/Control/Id.olean
 lib/lean/Init/Control/Id.olean.private
 lib/lean/Init/Control/Id.olean.server
 lib/lean/Init/Control/Lawful.ilean
+lib/lean/Init/Control/Lawful.ir
 lib/lean/Init/Control/Lawful.olean
 lib/lean/Init/Control/Lawful.olean.private
 lib/lean/Init/Control/Lawful.olean.server
 lib/lean/Init/Control/Lawful/Basic.ilean
+lib/lean/Init/Control/Lawful/Basic.ir
 lib/lean/Init/Control/Lawful/Basic.olean
 lib/lean/Init/Control/Lawful/Basic.olean.private
 lib/lean/Init/Control/Lawful/Basic.olean.server
 lib/lean/Init/Control/Lawful/Instances.ilean
+lib/lean/Init/Control/Lawful/Instances.ir
 lib/lean/Init/Control/Lawful/Instances.olean
 lib/lean/Init/Control/Lawful/Instances.olean.private
 lib/lean/Init/Control/Lawful/Instances.olean.server
 lib/lean/Init/Control/Lawful/Lemmas.ilean
+lib/lean/Init/Control/Lawful/Lemmas.ir
 lib/lean/Init/Control/Lawful/Lemmas.olean
 lib/lean/Init/Control/Lawful/Lemmas.olean.private
 lib/lean/Init/Control/Lawful/Lemmas.olean.server
+lib/lean/Init/Control/Lawful/MonadLift.ilean
+lib/lean/Init/Control/Lawful/MonadLift.ir
+lib/lean/Init/Control/Lawful/MonadLift.olean
+lib/lean/Init/Control/Lawful/MonadLift.olean.private
+lib/lean/Init/Control/Lawful/MonadLift.olean.server
+lib/lean/Init/Control/Lawful/MonadLift/Basic.ilean
+lib/lean/Init/Control/Lawful/MonadLift/Basic.ir
+lib/lean/Init/Control/Lawful/MonadLift/Basic.olean
+lib/lean/Init/Control/Lawful/MonadLift/Basic.olean.private
+lib/lean/Init/Control/Lawful/MonadLift/Basic.olean.server
+lib/lean/Init/Control/Lawful/MonadLift/Instances.ilean
+lib/lean/Init/Control/Lawful/MonadLift/Instances.ir
+lib/lean/Init/Control/Lawful/MonadLift/Instances.olean
+lib/lean/Init/Control/Lawful/MonadLift/Instances.olean.private
+lib/lean/Init/Control/Lawful/MonadLift/Instances.olean.server
+lib/lean/Init/Control/Lawful/MonadLift/Lemmas.ilean
+lib/lean/Init/Control/Lawful/MonadLift/Lemmas.ir
+lib/lean/Init/Control/Lawful/MonadLift/Lemmas.olean
+lib/lean/Init/Control/Lawful/MonadLift/Lemmas.olean.private
+lib/lean/Init/Control/Lawful/MonadLift/Lemmas.olean.server
 lib/lean/Init/Control/Option.ilean
+lib/lean/Init/Control/Option.ir
 lib/lean/Init/Control/Option.olean
 lib/lean/Init/Control/Option.olean.private
 lib/lean/Init/Control/Option.olean.server
 lib/lean/Init/Control/Reader.ilean
+lib/lean/Init/Control/Reader.ir
 lib/lean/Init/Control/Reader.olean
 lib/lean/Init/Control/Reader.olean.private
 lib/lean/Init/Control/Reader.olean.server
 lib/lean/Init/Control/State.ilean
+lib/lean/Init/Control/State.ir
 lib/lean/Init/Control/State.olean
 lib/lean/Init/Control/State.olean.private
 lib/lean/Init/Control/State.olean.server
 lib/lean/Init/Control/StateCps.ilean
+lib/lean/Init/Control/StateCps.ir
 lib/lean/Init/Control/StateCps.olean
 lib/lean/Init/Control/StateCps.olean.private
 lib/lean/Init/Control/StateCps.olean.server
 lib/lean/Init/Control/StateRef.ilean
+lib/lean/Init/Control/StateRef.ir
 lib/lean/Init/Control/StateRef.olean
 lib/lean/Init/Control/StateRef.olean.private
 lib/lean/Init/Control/StateRef.olean.server
 lib/lean/Init/Conv.ilean
+lib/lean/Init/Conv.ir
 lib/lean/Init/Conv.olean
 lib/lean/Init/Conv.olean.private
 lib/lean/Init/Conv.olean.server
 lib/lean/Init/Core.ilean
+lib/lean/Init/Core.ir
 lib/lean/Init/Core.olean
 lib/lean/Init/Core.olean.private
 lib/lean/Init/Core.olean.server
 lib/lean/Init/Data.ilean
+lib/lean/Init/Data.ir
 lib/lean/Init/Data.olean
 lib/lean/Init/Data.olean.private
 lib/lean/Init/Data.olean.server
 lib/lean/Init/Data/AC.ilean
+lib/lean/Init/Data/AC.ir
 lib/lean/Init/Data/AC.olean
 lib/lean/Init/Data/AC.olean.private
 lib/lean/Init/Data/AC.olean.server
 lib/lean/Init/Data/Array.ilean
+lib/lean/Init/Data/Array.ir
 lib/lean/Init/Data/Array.olean
 lib/lean/Init/Data/Array.olean.private
 lib/lean/Init/Data/Array.olean.server
 lib/lean/Init/Data/Array/Attach.ilean
+lib/lean/Init/Data/Array/Attach.ir
 lib/lean/Init/Data/Array/Attach.olean
 lib/lean/Init/Data/Array/Attach.olean.private
 lib/lean/Init/Data/Array/Attach.olean.server
 lib/lean/Init/Data/Array/Basic.ilean
+lib/lean/Init/Data/Array/Basic.ir
 lib/lean/Init/Data/Array/Basic.olean
 lib/lean/Init/Data/Array/Basic.olean.private
 lib/lean/Init/Data/Array/Basic.olean.server
 lib/lean/Init/Data/Array/BasicAux.ilean
+lib/lean/Init/Data/Array/BasicAux.ir
 lib/lean/Init/Data/Array/BasicAux.olean
 lib/lean/Init/Data/Array/BasicAux.olean.private
 lib/lean/Init/Data/Array/BasicAux.olean.server
 lib/lean/Init/Data/Array/BinSearch.ilean
+lib/lean/Init/Data/Array/BinSearch.ir
 lib/lean/Init/Data/Array/BinSearch.olean
 lib/lean/Init/Data/Array/BinSearch.olean.private
 lib/lean/Init/Data/Array/BinSearch.olean.server
 lib/lean/Init/Data/Array/Bootstrap.ilean
+lib/lean/Init/Data/Array/Bootstrap.ir
 lib/lean/Init/Data/Array/Bootstrap.olean
 lib/lean/Init/Data/Array/Bootstrap.olean.private
 lib/lean/Init/Data/Array/Bootstrap.olean.server
 lib/lean/Init/Data/Array/Count.ilean
+lib/lean/Init/Data/Array/Count.ir
 lib/lean/Init/Data/Array/Count.olean
 lib/lean/Init/Data/Array/Count.olean.private
 lib/lean/Init/Data/Array/Count.olean.server
 lib/lean/Init/Data/Array/DecidableEq.ilean
+lib/lean/Init/Data/Array/DecidableEq.ir
 lib/lean/Init/Data/Array/DecidableEq.olean
 lib/lean/Init/Data/Array/DecidableEq.olean.private
 lib/lean/Init/Data/Array/DecidableEq.olean.server
 lib/lean/Init/Data/Array/Erase.ilean
+lib/lean/Init/Data/Array/Erase.ir
 lib/lean/Init/Data/Array/Erase.olean
 lib/lean/Init/Data/Array/Erase.olean.private
 lib/lean/Init/Data/Array/Erase.olean.server
 lib/lean/Init/Data/Array/Extract.ilean
+lib/lean/Init/Data/Array/Extract.ir
 lib/lean/Init/Data/Array/Extract.olean
 lib/lean/Init/Data/Array/Extract.olean.private
 lib/lean/Init/Data/Array/Extract.olean.server
 lib/lean/Init/Data/Array/FinRange.ilean
+lib/lean/Init/Data/Array/FinRange.ir
 lib/lean/Init/Data/Array/FinRange.olean
 lib/lean/Init/Data/Array/FinRange.olean.private
 lib/lean/Init/Data/Array/FinRange.olean.server
 lib/lean/Init/Data/Array/Find.ilean
+lib/lean/Init/Data/Array/Find.ir
 lib/lean/Init/Data/Array/Find.olean
 lib/lean/Init/Data/Array/Find.olean.private
 lib/lean/Init/Data/Array/Find.olean.server
 lib/lean/Init/Data/Array/GetLit.ilean
+lib/lean/Init/Data/Array/GetLit.ir
 lib/lean/Init/Data/Array/GetLit.olean
 lib/lean/Init/Data/Array/GetLit.olean.private
 lib/lean/Init/Data/Array/GetLit.olean.server
 lib/lean/Init/Data/Array/InsertIdx.ilean
+lib/lean/Init/Data/Array/InsertIdx.ir
 lib/lean/Init/Data/Array/InsertIdx.olean
 lib/lean/Init/Data/Array/InsertIdx.olean.private
 lib/lean/Init/Data/Array/InsertIdx.olean.server
 lib/lean/Init/Data/Array/InsertionSort.ilean
+lib/lean/Init/Data/Array/InsertionSort.ir
 lib/lean/Init/Data/Array/InsertionSort.olean
 lib/lean/Init/Data/Array/InsertionSort.olean.private
 lib/lean/Init/Data/Array/InsertionSort.olean.server
 lib/lean/Init/Data/Array/Lemmas.ilean
+lib/lean/Init/Data/Array/Lemmas.ir
 lib/lean/Init/Data/Array/Lemmas.olean
 lib/lean/Init/Data/Array/Lemmas.olean.private
 lib/lean/Init/Data/Array/Lemmas.olean.server
 lib/lean/Init/Data/Array/Lex.ilean
+lib/lean/Init/Data/Array/Lex.ir
 lib/lean/Init/Data/Array/Lex.olean
 lib/lean/Init/Data/Array/Lex.olean.private
 lib/lean/Init/Data/Array/Lex.olean.server
 lib/lean/Init/Data/Array/Lex/Basic.ilean
+lib/lean/Init/Data/Array/Lex/Basic.ir
 lib/lean/Init/Data/Array/Lex/Basic.olean
 lib/lean/Init/Data/Array/Lex/Basic.olean.private
 lib/lean/Init/Data/Array/Lex/Basic.olean.server
 lib/lean/Init/Data/Array/Lex/Lemmas.ilean
+lib/lean/Init/Data/Array/Lex/Lemmas.ir
 lib/lean/Init/Data/Array/Lex/Lemmas.olean
 lib/lean/Init/Data/Array/Lex/Lemmas.olean.private
 lib/lean/Init/Data/Array/Lex/Lemmas.olean.server
 lib/lean/Init/Data/Array/MapIdx.ilean
+lib/lean/Init/Data/Array/MapIdx.ir
 lib/lean/Init/Data/Array/MapIdx.olean
 lib/lean/Init/Data/Array/MapIdx.olean.private
 lib/lean/Init/Data/Array/MapIdx.olean.server
 lib/lean/Init/Data/Array/Mem.ilean
+lib/lean/Init/Data/Array/Mem.ir
 lib/lean/Init/Data/Array/Mem.olean
 lib/lean/Init/Data/Array/Mem.olean.private
 lib/lean/Init/Data/Array/Mem.olean.server
 lib/lean/Init/Data/Array/Monadic.ilean
+lib/lean/Init/Data/Array/Monadic.ir
 lib/lean/Init/Data/Array/Monadic.olean
 lib/lean/Init/Data/Array/Monadic.olean.private
 lib/lean/Init/Data/Array/Monadic.olean.server
 lib/lean/Init/Data/Array/OfFn.ilean
+lib/lean/Init/Data/Array/OfFn.ir
 lib/lean/Init/Data/Array/OfFn.olean
 lib/lean/Init/Data/Array/OfFn.olean.private
 lib/lean/Init/Data/Array/OfFn.olean.server
 lib/lean/Init/Data/Array/Perm.ilean
+lib/lean/Init/Data/Array/Perm.ir
 lib/lean/Init/Data/Array/Perm.olean
 lib/lean/Init/Data/Array/Perm.olean.private
 lib/lean/Init/Data/Array/Perm.olean.server
 lib/lean/Init/Data/Array/QSort.ilean
+lib/lean/Init/Data/Array/QSort.ir
 lib/lean/Init/Data/Array/QSort.olean
 lib/lean/Init/Data/Array/QSort.olean.private
 lib/lean/Init/Data/Array/QSort.olean.server
 lib/lean/Init/Data/Array/QSort/Basic.ilean
+lib/lean/Init/Data/Array/QSort/Basic.ir
 lib/lean/Init/Data/Array/QSort/Basic.olean
 lib/lean/Init/Data/Array/QSort/Basic.olean.private
 lib/lean/Init/Data/Array/QSort/Basic.olean.server
 lib/lean/Init/Data/Array/Range.ilean
+lib/lean/Init/Data/Array/Range.ir
 lib/lean/Init/Data/Array/Range.olean
 lib/lean/Init/Data/Array/Range.olean.private
 lib/lean/Init/Data/Array/Range.olean.server
 lib/lean/Init/Data/Array/Set.ilean
+lib/lean/Init/Data/Array/Set.ir
 lib/lean/Init/Data/Array/Set.olean
 lib/lean/Init/Data/Array/Set.olean.private
 lib/lean/Init/Data/Array/Set.olean.server
 lib/lean/Init/Data/Array/Subarray.ilean
+lib/lean/Init/Data/Array/Subarray.ir
 lib/lean/Init/Data/Array/Subarray.olean
 lib/lean/Init/Data/Array/Subarray.olean.private
 lib/lean/Init/Data/Array/Subarray.olean.server
 lib/lean/Init/Data/Array/Subarray/Split.ilean
+lib/lean/Init/Data/Array/Subarray/Split.ir
 lib/lean/Init/Data/Array/Subarray/Split.olean
 lib/lean/Init/Data/Array/Subarray/Split.olean.private
 lib/lean/Init/Data/Array/Subarray/Split.olean.server
 lib/lean/Init/Data/Array/TakeDrop.ilean
+lib/lean/Init/Data/Array/TakeDrop.ir
 lib/lean/Init/Data/Array/TakeDrop.olean
 lib/lean/Init/Data/Array/TakeDrop.olean.private
 lib/lean/Init/Data/Array/TakeDrop.olean.server
 lib/lean/Init/Data/Array/Zip.ilean
+lib/lean/Init/Data/Array/Zip.ir
 lib/lean/Init/Data/Array/Zip.olean
 lib/lean/Init/Data/Array/Zip.olean.private
 lib/lean/Init/Data/Array/Zip.olean.server
 lib/lean/Init/Data/BEq.ilean
+lib/lean/Init/Data/BEq.ir
 lib/lean/Init/Data/BEq.olean
 lib/lean/Init/Data/BEq.olean.private
 lib/lean/Init/Data/BEq.olean.server
 lib/lean/Init/Data/Basic.ilean
+lib/lean/Init/Data/Basic.ir
 lib/lean/Init/Data/Basic.olean
 lib/lean/Init/Data/Basic.olean.private
 lib/lean/Init/Data/Basic.olean.server
 lib/lean/Init/Data/BitVec.ilean
+lib/lean/Init/Data/BitVec.ir
 lib/lean/Init/Data/BitVec.olean
 lib/lean/Init/Data/BitVec.olean.private
 lib/lean/Init/Data/BitVec.olean.server
 lib/lean/Init/Data/BitVec/Basic.ilean
+lib/lean/Init/Data/BitVec/Basic.ir
 lib/lean/Init/Data/BitVec/Basic.olean
 lib/lean/Init/Data/BitVec/Basic.olean.private
 lib/lean/Init/Data/BitVec/Basic.olean.server
 lib/lean/Init/Data/BitVec/BasicAux.ilean
+lib/lean/Init/Data/BitVec/BasicAux.ir
 lib/lean/Init/Data/BitVec/BasicAux.olean
 lib/lean/Init/Data/BitVec/BasicAux.olean.private
 lib/lean/Init/Data/BitVec/BasicAux.olean.server
 lib/lean/Init/Data/BitVec/Bitblast.ilean
+lib/lean/Init/Data/BitVec/Bitblast.ir
 lib/lean/Init/Data/BitVec/Bitblast.olean
 lib/lean/Init/Data/BitVec/Bitblast.olean.private
 lib/lean/Init/Data/BitVec/Bitblast.olean.server
+lib/lean/Init/Data/BitVec/Bootstrap.ilean
+lib/lean/Init/Data/BitVec/Bootstrap.ir
+lib/lean/Init/Data/BitVec/Bootstrap.olean
+lib/lean/Init/Data/BitVec/Bootstrap.olean.private
+lib/lean/Init/Data/BitVec/Bootstrap.olean.server
+lib/lean/Init/Data/BitVec/Decidable.ilean
+lib/lean/Init/Data/BitVec/Decidable.ir
+lib/lean/Init/Data/BitVec/Decidable.olean
+lib/lean/Init/Data/BitVec/Decidable.olean.private
+lib/lean/Init/Data/BitVec/Decidable.olean.server
 lib/lean/Init/Data/BitVec/Folds.ilean
+lib/lean/Init/Data/BitVec/Folds.ir
 lib/lean/Init/Data/BitVec/Folds.olean
 lib/lean/Init/Data/BitVec/Folds.olean.private
 lib/lean/Init/Data/BitVec/Folds.olean.server
 lib/lean/Init/Data/BitVec/Lemmas.ilean
+lib/lean/Init/Data/BitVec/Lemmas.ir
 lib/lean/Init/Data/BitVec/Lemmas.olean
 lib/lean/Init/Data/BitVec/Lemmas.olean.private
 lib/lean/Init/Data/BitVec/Lemmas.olean.server
 lib/lean/Init/Data/Bool.ilean
+lib/lean/Init/Data/Bool.ir
 lib/lean/Init/Data/Bool.olean
 lib/lean/Init/Data/Bool.olean.private
 lib/lean/Init/Data/Bool.olean.server
 lib/lean/Init/Data/ByteArray.ilean
+lib/lean/Init/Data/ByteArray.ir
 lib/lean/Init/Data/ByteArray.olean
 lib/lean/Init/Data/ByteArray.olean.private
 lib/lean/Init/Data/ByteArray.olean.server
 lib/lean/Init/Data/ByteArray/Basic.ilean
+lib/lean/Init/Data/ByteArray/Basic.ir
 lib/lean/Init/Data/ByteArray/Basic.olean
 lib/lean/Init/Data/ByteArray/Basic.olean.private
 lib/lean/Init/Data/ByteArray/Basic.olean.server
 lib/lean/Init/Data/Cast.ilean
+lib/lean/Init/Data/Cast.ir
 lib/lean/Init/Data/Cast.olean
 lib/lean/Init/Data/Cast.olean.private
 lib/lean/Init/Data/Cast.olean.server
 lib/lean/Init/Data/Char.ilean
+lib/lean/Init/Data/Char.ir
 lib/lean/Init/Data/Char.olean
 lib/lean/Init/Data/Char.olean.private
 lib/lean/Init/Data/Char.olean.server
 lib/lean/Init/Data/Char/Basic.ilean
+lib/lean/Init/Data/Char/Basic.ir
 lib/lean/Init/Data/Char/Basic.olean
 lib/lean/Init/Data/Char/Basic.olean.private
 lib/lean/Init/Data/Char/Basic.olean.server
 lib/lean/Init/Data/Char/Lemmas.ilean
+lib/lean/Init/Data/Char/Lemmas.ir
 lib/lean/Init/Data/Char/Lemmas.olean
 lib/lean/Init/Data/Char/Lemmas.olean.private
 lib/lean/Init/Data/Char/Lemmas.olean.server
 lib/lean/Init/Data/Fin.ilean
+lib/lean/Init/Data/Fin.ir
 lib/lean/Init/Data/Fin.olean
 lib/lean/Init/Data/Fin.olean.private
 lib/lean/Init/Data/Fin.olean.server
 lib/lean/Init/Data/Fin/Basic.ilean
+lib/lean/Init/Data/Fin/Basic.ir
 lib/lean/Init/Data/Fin/Basic.olean
 lib/lean/Init/Data/Fin/Basic.olean.private
 lib/lean/Init/Data/Fin/Basic.olean.server
 lib/lean/Init/Data/Fin/Bitwise.ilean
+lib/lean/Init/Data/Fin/Bitwise.ir
 lib/lean/Init/Data/Fin/Bitwise.olean
 lib/lean/Init/Data/Fin/Bitwise.olean.private
 lib/lean/Init/Data/Fin/Bitwise.olean.server
 lib/lean/Init/Data/Fin/Fold.ilean
+lib/lean/Init/Data/Fin/Fold.ir
 lib/lean/Init/Data/Fin/Fold.olean
 lib/lean/Init/Data/Fin/Fold.olean.private
 lib/lean/Init/Data/Fin/Fold.olean.server
 lib/lean/Init/Data/Fin/Iterate.ilean
+lib/lean/Init/Data/Fin/Iterate.ir
 lib/lean/Init/Data/Fin/Iterate.olean
 lib/lean/Init/Data/Fin/Iterate.olean.private
 lib/lean/Init/Data/Fin/Iterate.olean.server
 lib/lean/Init/Data/Fin/Lemmas.ilean
+lib/lean/Init/Data/Fin/Lemmas.ir
 lib/lean/Init/Data/Fin/Lemmas.olean
 lib/lean/Init/Data/Fin/Lemmas.olean.private
 lib/lean/Init/Data/Fin/Lemmas.olean.server
 lib/lean/Init/Data/Fin/Log2.ilean
+lib/lean/Init/Data/Fin/Log2.ir
 lib/lean/Init/Data/Fin/Log2.olean
 lib/lean/Init/Data/Fin/Log2.olean.private
 lib/lean/Init/Data/Fin/Log2.olean.server
 lib/lean/Init/Data/Float.ilean
+lib/lean/Init/Data/Float.ir
 lib/lean/Init/Data/Float.olean
 lib/lean/Init/Data/Float.olean.private
 lib/lean/Init/Data/Float.olean.server
 lib/lean/Init/Data/Float32.ilean
+lib/lean/Init/Data/Float32.ir
 lib/lean/Init/Data/Float32.olean
 lib/lean/Init/Data/Float32.olean.private
 lib/lean/Init/Data/Float32.olean.server
 lib/lean/Init/Data/FloatArray.ilean
+lib/lean/Init/Data/FloatArray.ir
 lib/lean/Init/Data/FloatArray.olean
 lib/lean/Init/Data/FloatArray.olean.private
 lib/lean/Init/Data/FloatArray.olean.server
 lib/lean/Init/Data/FloatArray/Basic.ilean
+lib/lean/Init/Data/FloatArray/Basic.ir
 lib/lean/Init/Data/FloatArray/Basic.olean
 lib/lean/Init/Data/FloatArray/Basic.olean.private
 lib/lean/Init/Data/FloatArray/Basic.olean.server
 lib/lean/Init/Data/Format.ilean
+lib/lean/Init/Data/Format.ir
 lib/lean/Init/Data/Format.olean
 lib/lean/Init/Data/Format.olean.private
 lib/lean/Init/Data/Format.olean.server
 lib/lean/Init/Data/Format/Basic.ilean
+lib/lean/Init/Data/Format/Basic.ir
 lib/lean/Init/Data/Format/Basic.olean
 lib/lean/Init/Data/Format/Basic.olean.private
 lib/lean/Init/Data/Format/Basic.olean.server
 lib/lean/Init/Data/Format/Instances.ilean
+lib/lean/Init/Data/Format/Instances.ir
 lib/lean/Init/Data/Format/Instances.olean
 lib/lean/Init/Data/Format/Instances.olean.private
 lib/lean/Init/Data/Format/Instances.olean.server
 lib/lean/Init/Data/Format/Macro.ilean
+lib/lean/Init/Data/Format/Macro.ir
 lib/lean/Init/Data/Format/Macro.olean
 lib/lean/Init/Data/Format/Macro.olean.private
 lib/lean/Init/Data/Format/Macro.olean.server
 lib/lean/Init/Data/Format/Syntax.ilean
+lib/lean/Init/Data/Format/Syntax.ir
 lib/lean/Init/Data/Format/Syntax.olean
 lib/lean/Init/Data/Format/Syntax.olean.private
 lib/lean/Init/Data/Format/Syntax.olean.server
 lib/lean/Init/Data/Function.ilean
+lib/lean/Init/Data/Function.ir
 lib/lean/Init/Data/Function.olean
 lib/lean/Init/Data/Function.olean.private
 lib/lean/Init/Data/Function.olean.server
 lib/lean/Init/Data/Hashable.ilean
+lib/lean/Init/Data/Hashable.ir
 lib/lean/Init/Data/Hashable.olean
 lib/lean/Init/Data/Hashable.olean.private
 lib/lean/Init/Data/Hashable.olean.server
 lib/lean/Init/Data/Int.ilean
+lib/lean/Init/Data/Int.ir
 lib/lean/Init/Data/Int.olean
 lib/lean/Init/Data/Int.olean.private
 lib/lean/Init/Data/Int.olean.server
 lib/lean/Init/Data/Int/Basic.ilean
+lib/lean/Init/Data/Int/Basic.ir
 lib/lean/Init/Data/Int/Basic.olean
 lib/lean/Init/Data/Int/Basic.olean.private
 lib/lean/Init/Data/Int/Basic.olean.server
 lib/lean/Init/Data/Int/Bitwise.ilean
+lib/lean/Init/Data/Int/Bitwise.ir
 lib/lean/Init/Data/Int/Bitwise.olean
 lib/lean/Init/Data/Int/Bitwise.olean.private
 lib/lean/Init/Data/Int/Bitwise.olean.server
 lib/lean/Init/Data/Int/Bitwise/Basic.ilean
+lib/lean/Init/Data/Int/Bitwise/Basic.ir
 lib/lean/Init/Data/Int/Bitwise/Basic.olean
 lib/lean/Init/Data/Int/Bitwise/Basic.olean.private
 lib/lean/Init/Data/Int/Bitwise/Basic.olean.server
 lib/lean/Init/Data/Int/Bitwise/Lemmas.ilean
+lib/lean/Init/Data/Int/Bitwise/Lemmas.ir
 lib/lean/Init/Data/Int/Bitwise/Lemmas.olean
 lib/lean/Init/Data/Int/Bitwise/Lemmas.olean.private
 lib/lean/Init/Data/Int/Bitwise/Lemmas.olean.server
 lib/lean/Init/Data/Int/Compare.ilean
+lib/lean/Init/Data/Int/Compare.ir
 lib/lean/Init/Data/Int/Compare.olean
 lib/lean/Init/Data/Int/Compare.olean.private
 lib/lean/Init/Data/Int/Compare.olean.server
 lib/lean/Init/Data/Int/Cooper.ilean
+lib/lean/Init/Data/Int/Cooper.ir
 lib/lean/Init/Data/Int/Cooper.olean
 lib/lean/Init/Data/Int/Cooper.olean.private
 lib/lean/Init/Data/Int/Cooper.olean.server
 lib/lean/Init/Data/Int/DivMod.ilean
+lib/lean/Init/Data/Int/DivMod.ir
 lib/lean/Init/Data/Int/DivMod.olean
 lib/lean/Init/Data/Int/DivMod.olean.private
 lib/lean/Init/Data/Int/DivMod.olean.server
 lib/lean/Init/Data/Int/DivMod/Basic.ilean
+lib/lean/Init/Data/Int/DivMod/Basic.ir
 lib/lean/Init/Data/Int/DivMod/Basic.olean
 lib/lean/Init/Data/Int/DivMod/Basic.olean.private
 lib/lean/Init/Data/Int/DivMod/Basic.olean.server
 lib/lean/Init/Data/Int/DivMod/Bootstrap.ilean
+lib/lean/Init/Data/Int/DivMod/Bootstrap.ir
 lib/lean/Init/Data/Int/DivMod/Bootstrap.olean
 lib/lean/Init/Data/Int/DivMod/Bootstrap.olean.private
 lib/lean/Init/Data/Int/DivMod/Bootstrap.olean.server
 lib/lean/Init/Data/Int/DivMod/Lemmas.ilean
+lib/lean/Init/Data/Int/DivMod/Lemmas.ir
 lib/lean/Init/Data/Int/DivMod/Lemmas.olean
 lib/lean/Init/Data/Int/DivMod/Lemmas.olean.private
 lib/lean/Init/Data/Int/DivMod/Lemmas.olean.server
 lib/lean/Init/Data/Int/Gcd.ilean
+lib/lean/Init/Data/Int/Gcd.ir
 lib/lean/Init/Data/Int/Gcd.olean
 lib/lean/Init/Data/Int/Gcd.olean.private
 lib/lean/Init/Data/Int/Gcd.olean.server
 lib/lean/Init/Data/Int/Lemmas.ilean
+lib/lean/Init/Data/Int/Lemmas.ir
 lib/lean/Init/Data/Int/Lemmas.olean
 lib/lean/Init/Data/Int/Lemmas.olean.private
 lib/lean/Init/Data/Int/Lemmas.olean.server
 lib/lean/Init/Data/Int/LemmasAux.ilean
+lib/lean/Init/Data/Int/LemmasAux.ir
 lib/lean/Init/Data/Int/LemmasAux.olean
 lib/lean/Init/Data/Int/LemmasAux.olean.private
 lib/lean/Init/Data/Int/LemmasAux.olean.server
 lib/lean/Init/Data/Int/Linear.ilean
+lib/lean/Init/Data/Int/Linear.ir
 lib/lean/Init/Data/Int/Linear.olean
 lib/lean/Init/Data/Int/Linear.olean.private
 lib/lean/Init/Data/Int/Linear.olean.server
 lib/lean/Init/Data/Int/OfNat.ilean
+lib/lean/Init/Data/Int/OfNat.ir
 lib/lean/Init/Data/Int/OfNat.olean
 lib/lean/Init/Data/Int/OfNat.olean.private
 lib/lean/Init/Data/Int/OfNat.olean.server
 lib/lean/Init/Data/Int/Order.ilean
+lib/lean/Init/Data/Int/Order.ir
 lib/lean/Init/Data/Int/Order.olean
 lib/lean/Init/Data/Int/Order.olean.private
 lib/lean/Init/Data/Int/Order.olean.server
 lib/lean/Init/Data/Int/Pow.ilean
+lib/lean/Init/Data/Int/Pow.ir
 lib/lean/Init/Data/Int/Pow.olean
 lib/lean/Init/Data/Int/Pow.olean.private
 lib/lean/Init/Data/Int/Pow.olean.server
+lib/lean/Init/Data/Iterators.ilean
+lib/lean/Init/Data/Iterators.ir
+lib/lean/Init/Data/Iterators.olean
+lib/lean/Init/Data/Iterators.olean.private
+lib/lean/Init/Data/Iterators.olean.server
+lib/lean/Init/Data/Iterators/Basic.ilean
+lib/lean/Init/Data/Iterators/Basic.ir
+lib/lean/Init/Data/Iterators/Basic.olean
+lib/lean/Init/Data/Iterators/Basic.olean.private
+lib/lean/Init/Data/Iterators/Basic.olean.server
+lib/lean/Init/Data/Iterators/Combinators.ilean
+lib/lean/Init/Data/Iterators/Combinators.ir
+lib/lean/Init/Data/Iterators/Combinators.olean
+lib/lean/Init/Data/Iterators/Combinators.olean.private
+lib/lean/Init/Data/Iterators/Combinators.olean.server
+lib/lean/Init/Data/Iterators/Combinators/Attach.ilean
+lib/lean/Init/Data/Iterators/Combinators/Attach.ir
+lib/lean/Init/Data/Iterators/Combinators/Attach.olean
+lib/lean/Init/Data/Iterators/Combinators/Attach.olean.private
+lib/lean/Init/Data/Iterators/Combinators/Attach.olean.server
+lib/lean/Init/Data/Iterators/Combinators/FilterMap.ilean
+lib/lean/Init/Data/Iterators/Combinators/FilterMap.ir
+lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean
+lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean.private
+lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean.server
+lib/lean/Init/Data/Iterators/Combinators/Monadic.ilean
+lib/lean/Init/Data/Iterators/Combinators/Monadic.ir
+lib/lean/Init/Data/Iterators/Combinators/Monadic.olean
+lib/lean/Init/Data/Iterators/Combinators/Monadic.olean.private
+lib/lean/Init/Data/Iterators/Combinators/Monadic.olean.server
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.ilean
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.ir
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.olean
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.olean.private
+lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.olean.server
+lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.ilean
+lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.ir
+lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean
+lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean.private
+lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean.server
+lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.ilean
+lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.ir
+lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean
+lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean.private
+lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean.server
+lib/lean/Init/Data/Iterators/Combinators/ULift.ilean
+lib/lean/Init/Data/Iterators/Combinators/ULift.ir
+lib/lean/Init/Data/Iterators/Combinators/ULift.olean
+lib/lean/Init/Data/Iterators/Combinators/ULift.olean.private
+lib/lean/Init/Data/Iterators/Combinators/ULift.olean.server
+lib/lean/Init/Data/Iterators/Consumers.ilean
+lib/lean/Init/Data/Iterators/Consumers.ir
+lib/lean/Init/Data/Iterators/Consumers.olean
+lib/lean/Init/Data/Iterators/Consumers.olean.private
+lib/lean/Init/Data/Iterators/Consumers.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Access.ilean
+lib/lean/Init/Data/Iterators/Consumers/Access.ir
+lib/lean/Init/Data/Iterators/Consumers/Access.olean
+lib/lean/Init/Data/Iterators/Consumers/Access.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Access.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Collect.ilean
+lib/lean/Init/Data/Iterators/Consumers/Collect.ir
+lib/lean/Init/Data/Iterators/Consumers/Collect.olean
+lib/lean/Init/Data/Iterators/Consumers/Collect.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Collect.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Loop.ilean
+lib/lean/Init/Data/Iterators/Consumers/Loop.ir
+lib/lean/Init/Data/Iterators/Consumers/Loop.olean
+lib/lean/Init/Data/Iterators/Consumers/Loop.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Loop.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Monadic.ilean
+lib/lean/Init/Data/Iterators/Consumers/Monadic.ir
+lib/lean/Init/Data/Iterators/Consumers/Monadic.olean
+lib/lean/Init/Data/Iterators/Consumers/Monadic.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Monadic.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Access.ilean
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Access.ir
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Access.olean
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Access.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Access.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Collect.ilean
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Collect.ir
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Collect.olean
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Collect.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Collect.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Loop.ilean
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Loop.ir
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Loop.olean
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Loop.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Loop.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.ilean
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.ir
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.olean
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.olean.server
+lib/lean/Init/Data/Iterators/Consumers/Partial.ilean
+lib/lean/Init/Data/Iterators/Consumers/Partial.ir
+lib/lean/Init/Data/Iterators/Consumers/Partial.olean
+lib/lean/Init/Data/Iterators/Consumers/Partial.olean.private
+lib/lean/Init/Data/Iterators/Consumers/Partial.olean.server
+lib/lean/Init/Data/Iterators/Internal.ilean
+lib/lean/Init/Data/Iterators/Internal.ir
+lib/lean/Init/Data/Iterators/Internal.olean
+lib/lean/Init/Data/Iterators/Internal.olean.private
+lib/lean/Init/Data/Iterators/Internal.olean.server
+lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.ilean
+lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.ir
+lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.olean
+lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.olean.private
+lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.olean.server
+lib/lean/Init/Data/Iterators/Internal/Termination.ilean
+lib/lean/Init/Data/Iterators/Internal/Termination.ir
+lib/lean/Init/Data/Iterators/Internal/Termination.olean
+lib/lean/Init/Data/Iterators/Internal/Termination.olean.private
+lib/lean/Init/Data/Iterators/Internal/Termination.olean.server
+lib/lean/Init/Data/Iterators/Lemmas.ilean
+lib/lean/Init/Data/Iterators/Lemmas.ir
+lib/lean/Init/Data/Iterators/Lemmas.olean
+lib/lean/Init/Data/Iterators/Lemmas.olean.private
+lib/lean/Init/Data/Iterators/Lemmas.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Basic.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Basic.ir
+lib/lean/Init/Data/Iterators/Lemmas/Basic.olean
+lib/lean/Init/Data/Iterators/Lemmas/Basic.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Basic.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Attach.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Attach.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Attach.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Attach.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Attach.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/FilterMap.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.ir
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.olean
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Consumers.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers.ir
+lib/lean/Init/Data/Iterators/Lemmas/Consumers.olean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Consumers.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Collect.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Collect.ir
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Collect.olean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Collect.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Collect.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Loop.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Loop.ir
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Loop.olean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Loop.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Loop.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic.ir
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic.olean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.ir
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.olean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.ir
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.olean
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.olean.server
+lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.ilean
+lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.ir
+lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean
+lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean.private
+lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean.server
+lib/lean/Init/Data/Iterators/PostconditionMonad.ilean
+lib/lean/Init/Data/Iterators/PostconditionMonad.ir
+lib/lean/Init/Data/Iterators/PostconditionMonad.olean
+lib/lean/Init/Data/Iterators/PostconditionMonad.olean.private
+lib/lean/Init/Data/Iterators/PostconditionMonad.olean.server
+lib/lean/Init/Data/Iterators/ToIterator.ilean
+lib/lean/Init/Data/Iterators/ToIterator.ir
+lib/lean/Init/Data/Iterators/ToIterator.olean
+lib/lean/Init/Data/Iterators/ToIterator.olean.private
+lib/lean/Init/Data/Iterators/ToIterator.olean.server
 lib/lean/Init/Data/List.ilean
+lib/lean/Init/Data/List.ir
 lib/lean/Init/Data/List.olean
 lib/lean/Init/Data/List.olean.private
 lib/lean/Init/Data/List.olean.server
 lib/lean/Init/Data/List/Attach.ilean
+lib/lean/Init/Data/List/Attach.ir
 lib/lean/Init/Data/List/Attach.olean
 lib/lean/Init/Data/List/Attach.olean.private
 lib/lean/Init/Data/List/Attach.olean.server
 lib/lean/Init/Data/List/Basic.ilean
+lib/lean/Init/Data/List/Basic.ir
 lib/lean/Init/Data/List/Basic.olean
 lib/lean/Init/Data/List/Basic.olean.private
 lib/lean/Init/Data/List/Basic.olean.server
 lib/lean/Init/Data/List/BasicAux.ilean
+lib/lean/Init/Data/List/BasicAux.ir
 lib/lean/Init/Data/List/BasicAux.olean
 lib/lean/Init/Data/List/BasicAux.olean.private
 lib/lean/Init/Data/List/BasicAux.olean.server
 lib/lean/Init/Data/List/Control.ilean
+lib/lean/Init/Data/List/Control.ir
 lib/lean/Init/Data/List/Control.olean
 lib/lean/Init/Data/List/Control.olean.private
 lib/lean/Init/Data/List/Control.olean.server
 lib/lean/Init/Data/List/Count.ilean
+lib/lean/Init/Data/List/Count.ir
 lib/lean/Init/Data/List/Count.olean
 lib/lean/Init/Data/List/Count.olean.private
 lib/lean/Init/Data/List/Count.olean.server
 lib/lean/Init/Data/List/Erase.ilean
+lib/lean/Init/Data/List/Erase.ir
 lib/lean/Init/Data/List/Erase.olean
 lib/lean/Init/Data/List/Erase.olean.private
 lib/lean/Init/Data/List/Erase.olean.server
 lib/lean/Init/Data/List/FinRange.ilean
+lib/lean/Init/Data/List/FinRange.ir
 lib/lean/Init/Data/List/FinRange.olean
 lib/lean/Init/Data/List/FinRange.olean.private
 lib/lean/Init/Data/List/FinRange.olean.server
 lib/lean/Init/Data/List/Find.ilean
+lib/lean/Init/Data/List/Find.ir
 lib/lean/Init/Data/List/Find.olean
 lib/lean/Init/Data/List/Find.olean.private
 lib/lean/Init/Data/List/Find.olean.server
 lib/lean/Init/Data/List/Impl.ilean
+lib/lean/Init/Data/List/Impl.ir
 lib/lean/Init/Data/List/Impl.olean
 lib/lean/Init/Data/List/Impl.olean.private
 lib/lean/Init/Data/List/Impl.olean.server
 lib/lean/Init/Data/List/Lemmas.ilean
+lib/lean/Init/Data/List/Lemmas.ir
 lib/lean/Init/Data/List/Lemmas.olean
 lib/lean/Init/Data/List/Lemmas.olean.private
 lib/lean/Init/Data/List/Lemmas.olean.server
 lib/lean/Init/Data/List/Lex.ilean
+lib/lean/Init/Data/List/Lex.ir
 lib/lean/Init/Data/List/Lex.olean
 lib/lean/Init/Data/List/Lex.olean.private
 lib/lean/Init/Data/List/Lex.olean.server
 lib/lean/Init/Data/List/MapIdx.ilean
+lib/lean/Init/Data/List/MapIdx.ir
 lib/lean/Init/Data/List/MapIdx.olean
 lib/lean/Init/Data/List/MapIdx.olean.private
 lib/lean/Init/Data/List/MapIdx.olean.server
 lib/lean/Init/Data/List/MinMax.ilean
+lib/lean/Init/Data/List/MinMax.ir
 lib/lean/Init/Data/List/MinMax.olean
 lib/lean/Init/Data/List/MinMax.olean.private
 lib/lean/Init/Data/List/MinMax.olean.server
 lib/lean/Init/Data/List/Monadic.ilean
+lib/lean/Init/Data/List/Monadic.ir
 lib/lean/Init/Data/List/Monadic.olean
 lib/lean/Init/Data/List/Monadic.olean.private
 lib/lean/Init/Data/List/Monadic.olean.server
 lib/lean/Init/Data/List/Nat.ilean
+lib/lean/Init/Data/List/Nat.ir
 lib/lean/Init/Data/List/Nat.olean
 lib/lean/Init/Data/List/Nat.olean.private
 lib/lean/Init/Data/List/Nat.olean.server
 lib/lean/Init/Data/List/Nat/BEq.ilean
+lib/lean/Init/Data/List/Nat/BEq.ir
 lib/lean/Init/Data/List/Nat/BEq.olean
 lib/lean/Init/Data/List/Nat/BEq.olean.private
 lib/lean/Init/Data/List/Nat/BEq.olean.server
 lib/lean/Init/Data/List/Nat/Basic.ilean
+lib/lean/Init/Data/List/Nat/Basic.ir
 lib/lean/Init/Data/List/Nat/Basic.olean
 lib/lean/Init/Data/List/Nat/Basic.olean.private
 lib/lean/Init/Data/List/Nat/Basic.olean.server
 lib/lean/Init/Data/List/Nat/Count.ilean
+lib/lean/Init/Data/List/Nat/Count.ir
 lib/lean/Init/Data/List/Nat/Count.olean
 lib/lean/Init/Data/List/Nat/Count.olean.private
 lib/lean/Init/Data/List/Nat/Count.olean.server
 lib/lean/Init/Data/List/Nat/Erase.ilean
+lib/lean/Init/Data/List/Nat/Erase.ir
 lib/lean/Init/Data/List/Nat/Erase.olean
 lib/lean/Init/Data/List/Nat/Erase.olean.private
 lib/lean/Init/Data/List/Nat/Erase.olean.server
 lib/lean/Init/Data/List/Nat/Find.ilean
+lib/lean/Init/Data/List/Nat/Find.ir
 lib/lean/Init/Data/List/Nat/Find.olean
 lib/lean/Init/Data/List/Nat/Find.olean.private
 lib/lean/Init/Data/List/Nat/Find.olean.server
 lib/lean/Init/Data/List/Nat/InsertIdx.ilean
+lib/lean/Init/Data/List/Nat/InsertIdx.ir
 lib/lean/Init/Data/List/Nat/InsertIdx.olean
 lib/lean/Init/Data/List/Nat/InsertIdx.olean.private
 lib/lean/Init/Data/List/Nat/InsertIdx.olean.server
 lib/lean/Init/Data/List/Nat/Modify.ilean
+lib/lean/Init/Data/List/Nat/Modify.ir
 lib/lean/Init/Data/List/Nat/Modify.olean
 lib/lean/Init/Data/List/Nat/Modify.olean.private
 lib/lean/Init/Data/List/Nat/Modify.olean.server
 lib/lean/Init/Data/List/Nat/Pairwise.ilean
+lib/lean/Init/Data/List/Nat/Pairwise.ir
 lib/lean/Init/Data/List/Nat/Pairwise.olean
 lib/lean/Init/Data/List/Nat/Pairwise.olean.private
 lib/lean/Init/Data/List/Nat/Pairwise.olean.server
 lib/lean/Init/Data/List/Nat/Perm.ilean
+lib/lean/Init/Data/List/Nat/Perm.ir
 lib/lean/Init/Data/List/Nat/Perm.olean
 lib/lean/Init/Data/List/Nat/Perm.olean.private
 lib/lean/Init/Data/List/Nat/Perm.olean.server
 lib/lean/Init/Data/List/Nat/Range.ilean
+lib/lean/Init/Data/List/Nat/Range.ir
 lib/lean/Init/Data/List/Nat/Range.olean
 lib/lean/Init/Data/List/Nat/Range.olean.private
 lib/lean/Init/Data/List/Nat/Range.olean.server
 lib/lean/Init/Data/List/Nat/Sublist.ilean
+lib/lean/Init/Data/List/Nat/Sublist.ir
 lib/lean/Init/Data/List/Nat/Sublist.olean
 lib/lean/Init/Data/List/Nat/Sublist.olean.private
 lib/lean/Init/Data/List/Nat/Sublist.olean.server
 lib/lean/Init/Data/List/Nat/TakeDrop.ilean
+lib/lean/Init/Data/List/Nat/TakeDrop.ir
 lib/lean/Init/Data/List/Nat/TakeDrop.olean
 lib/lean/Init/Data/List/Nat/TakeDrop.olean.private
 lib/lean/Init/Data/List/Nat/TakeDrop.olean.server
 lib/lean/Init/Data/List/Notation.ilean
+lib/lean/Init/Data/List/Notation.ir
 lib/lean/Init/Data/List/Notation.olean
 lib/lean/Init/Data/List/Notation.olean.private
 lib/lean/Init/Data/List/Notation.olean.server
 lib/lean/Init/Data/List/OfFn.ilean
+lib/lean/Init/Data/List/OfFn.ir
 lib/lean/Init/Data/List/OfFn.olean
 lib/lean/Init/Data/List/OfFn.olean.private
 lib/lean/Init/Data/List/OfFn.olean.server
 lib/lean/Init/Data/List/Pairwise.ilean
+lib/lean/Init/Data/List/Pairwise.ir
 lib/lean/Init/Data/List/Pairwise.olean
 lib/lean/Init/Data/List/Pairwise.olean.private
 lib/lean/Init/Data/List/Pairwise.olean.server
 lib/lean/Init/Data/List/Perm.ilean
*** 2554 LINES SKIPPED ***