~cypheon/Idris2

8bef973991c782775d178917b18dc050a83b8ef1 — Johann Rudloff a month ago 1e178a6 + 3c532ea
Merge remote-tracking branch 'origin/main'
564 files changed, 18807 insertions(+), 13408 deletions(-)

M .github/workflows/ci-idris2.yml
M .gitignore
M CHANGELOG.md
M CONTRIBUTORS
M INSTALL.md
M Makefile
M bootstrap/idris2-boot.sh
M bootstrap/idris2-rktboot.sh
M bootstrap/idris2_app/idris2.rkt
M bootstrap/idris2_app/idris2.ss
M docs/source/backends/index.rst
A docs/source/backends/libraries.rst
M docs/source/implementation/ide-protocol.rst
M docs/source/implementation/overview.rst
M docs/source/reference/builtins.rst
M docs/source/reference/index.rst
M docs/source/reference/literate.rst
A docs/source/reference/pragmas.rst
M docs/source/reference/records.rst
M docs/source/tutorial/starting.rst
M docs/source/tutorial/typesfuns.rst
M docs/source/tutorial/views.rst
M docs/source/typedd/typedd.rst
M docs/source/updates/updates.rst
M idris2api.ipkg
A idris2protocols.ipkg.hide
M libs/base/Control/App/Console.idr
M libs/base/Control/App/FileIO.idr
A libs/base/Control/Function.idr
M libs/base/Control/Monad/Identity.idr
M libs/base/Control/Monad/RWS/CPS.idr
M libs/base/Control/Monad/Writer/CPS.idr
M libs/base/Control/Relation.idr
M libs/base/Control/WellFounded.idr
M libs/base/Data/Bifoldable.idr
M libs/base/Data/Bits.idr
M libs/base/Data/Colist.idr
M libs/base/Data/Colist1.idr
M libs/base/Data/Contravariant.idr
M libs/base/Data/Either.idr
M libs/base/Data/Fin.idr
M libs/base/Data/Fin/Order.idr
M libs/base/Data/IOArray.idr
M libs/base/Data/List.idr
M libs/base/Data/List/Elem.idr
M libs/base/Data/List/Quantifiers.idr
M libs/base/Data/List/Views.idr
M libs/base/Data/List1.idr
M libs/base/Data/Maybe.idr
M libs/base/Data/Nat.idr
M libs/base/Data/Nat/Order.idr
M libs/base/Data/SnocList.idr
M libs/base/Data/SnocList/Elem.idr
M libs/base/Data/Stream.idr
M libs/base/Data/String.idr
M libs/base/Data/Vect.idr
M libs/base/Decidable/Decidable.idr
M libs/base/Decidable/Equality.idr
M libs/base/Language/Reflection.idr
M libs/base/Language/Reflection/TT.idr
M libs/base/Language/Reflection/TTImp.idr
M libs/base/System.idr
M libs/base/System/Clock.idr
M libs/base/System/Concurrency.idr
M libs/base/System/Directory.idr
M libs/base/System/Errno.idr
A libs/base/System/Escape.idr
M libs/base/System/FFI.idr
M libs/base/System/File.idr
M libs/base/System/File/Buffer.idr
M libs/base/System/File/Error.idr
M libs/base/System/File/Handle.idr
M libs/base/System/File/Meta.idr
M libs/base/System/File/Mode.idr
M libs/base/System/File/Permissions.idr
M libs/base/System/File/Process.idr
M libs/base/System/File/ReadWrite.idr
M libs/base/System/File/Support.idr
M libs/base/System/File/Types.idr
M libs/base/System/File/Virtual.idr
M libs/base/System/Info.idr
M libs/base/System/REPL.idr
M libs/base/System/Signal.idr
M libs/base/base.ipkg
M libs/contrib/Control/Linear/LIO.idr
M libs/contrib/Control/Validation.idr
M libs/contrib/Data/Binary.idr
M libs/contrib/Data/Bool/Decidable.idr
M libs/contrib/Data/Container.idr
A libs/contrib/Data/List/Alternating.idr
M libs/contrib/Data/List/Extra.idr
M libs/contrib/Data/List/HasLength.idr
M libs/contrib/Data/List/Palindrome.idr
M libs/contrib/Data/List/Reverse.idr
M libs/contrib/Data/List/TailRec.idr
M libs/contrib/Data/Monoid/Exponentiation.idr
M libs/contrib/Data/Nat/Division.idr
M libs/contrib/Data/Nat/Equational.idr
M libs/contrib/Data/Nat/Exponentiation.idr
M libs/contrib/Data/Nat/Factor.idr
M libs/contrib/Data/Nat/Order/Properties.idr
M libs/contrib/Data/Nat/Order/Strict.idr
D libs/contrib/Data/Num/Implementations.idr
M libs/contrib/Data/SortedMap.idr
M libs/contrib/Data/String/Extra.idr
M libs/contrib/Data/String/Interpolation.idr
M libs/contrib/Data/String/Parser.idr
M libs/contrib/Data/String/Parser/Expression.idr
M libs/contrib/Data/Telescope/Congruence.idr
M libs/contrib/Data/Telescope/Telescope.idr
M libs/contrib/Data/Tree/Perfect.idr
M libs/contrib/Data/Vect/Binary.idr
M libs/contrib/Data/Vect/Properties/Foldr.idr
M libs/contrib/Data/Vect/Properties/Map.idr
M libs/contrib/Data/Void.idr
M libs/contrib/Decidable/Order/Strict.idr
M libs/contrib/Language/JSON/Data.idr
M libs/contrib/Language/JSON/Lexer.idr
M libs/contrib/Language/JSON/Parser.idr
M libs/contrib/Language/JSON/String/Tokens.idr
M libs/contrib/Syntax/PreorderReasoning/Generic.idr
M libs/contrib/System/Console/GetOpt.idr
M libs/contrib/System/Directory/Tree.idr
M libs/contrib/System/Path.idr
M libs/contrib/Text/Lexer/Core.idr
M libs/contrib/Text/Lexer/Tokenizer.idr
M libs/contrib/Text/Literate.idr
M libs/contrib/Text/Parser.idr
M libs/contrib/Text/Parser/Expression.idr
M libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr
M libs/contrib/Text/PrettyPrint/Prettyprinter/Render/HTML.idr
M libs/contrib/Text/PrettyPrint/Prettyprinter/Render/String.idr
M libs/contrib/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr
M libs/contrib/Text/PrettyPrint/Prettyprinter/Util.idr
M libs/contrib/contrib.ipkg
M libs/prelude/Builtin.idr
M libs/prelude/Prelude/Cast.idr
M libs/prelude/Prelude/EqOrd.idr
M libs/prelude/Prelude/Interfaces.idr
M libs/prelude/Prelude/Interpolation.idr
M libs/prelude/Prelude/Num.idr
M libs/prelude/Prelude/Show.idr
M libs/prelude/Prelude/Types.idr
M libs/prelude/Prelude/Uninhabited.idr
M libs/test/Test/Golden.idr
M samples/Vect.idr
M samples/deprec.idr
M src/Compiler/ANF.idr
M src/Compiler/CaseOpts.idr
M src/Compiler/Common.idr
M src/Compiler/CompileExpr.idr
M src/Compiler/ES/Ast.idr
M src/Compiler/ES/Codegen.idr
M src/Compiler/ES/Javascript.idr
M src/Compiler/ES/Node.idr
M src/Compiler/ES/State.idr
M src/Compiler/ES/TailRec.idr
M src/Compiler/ES/ToAst.idr
M src/Compiler/Inline.idr
M src/Compiler/Interpreter/VMCode.idr
M src/Compiler/LambdaLift.idr
A src/Compiler/NoMangle.idr
M src/Compiler/Opts/CSE.idr
M src/Compiler/Opts/InlineHeuristics.idr
M src/Compiler/RefC/CC.idr
M src/Compiler/RefC/RefC.idr
M src/Compiler/Scheme/Chez.idr
M src/Compiler/Scheme/ChezSep.idr
M src/Compiler/Scheme/Common.idr
M src/Compiler/Scheme/Gambit.idr
M src/Compiler/Scheme/Racket.idr
M src/Compiler/VMCode.idr
M src/Core/Binary.idr
M src/Core/Binary/Prims.idr
M src/Core/Case/CaseBuilder.idr
M src/Core/Case/CaseTree.idr
M src/Core/Case/Util.idr
M src/Core/CompileExpr.idr
M src/Core/Context.idr
M src/Core/Context/Context.idr
M src/Core/Context/Data.idr
M src/Core/Context/Log.idr
M src/Core/Core.idr
M src/Core/Coverage.idr
M src/Core/Directory.idr
M src/Core/GetType.idr
M src/Core/Hash.idr
M src/Core/InitPrimitives.idr
M src/Core/LinearCheck.idr
M src/Core/Metadata.idr
M src/Core/Name.idr
M src/Core/Name/Namespace.idr
M src/Core/Normalise.idr
M src/Core/Normalise/Convert.idr
M src/Core/Normalise/Eval.idr
M src/Core/Normalise/Quote.idr
M src/Core/Options.idr
M src/Core/Options/Log.idr
M src/Core/Ord.idr
M src/Core/Primitives.idr
M src/Core/SchemeEval.idr
M src/Core/SchemeEval/Compile.idr
M src/Core/SchemeEval/Evaluate.idr
M src/Core/SchemeEval/Quote.idr
M src/Core/TT.idr
M src/Core/TT/Traversals.idr
M src/Core/TTC.idr
M src/Core/Termination.idr
M src/Core/Transform.idr
M src/Core/Unify.idr
M src/Core/UnifyState.idr
M src/Core/Value.idr
M src/Idris/CommandLine.idr
M src/Idris/Desugar.idr
M src/Idris/Desugar/Mutual.idr
A src/Idris/Doc/Annotations.idr
M src/Idris/Doc/HTML.idr
A src/Idris/Doc/Keywords.idr
M src/Idris/Doc/String.idr
M src/Idris/Driver.idr
M src/Idris/Elab/Implementation.idr
M src/Idris/Elab/Interface.idr
M src/Idris/Error.idr
M src/Idris/IDEMode/CaseSplit.idr
M src/Idris/IDEMode/Commands.idr
M src/Idris/IDEMode/Holes.idr
M src/Idris/IDEMode/Parser.idr
A src/Idris/IDEMode/Pretty.idr
M src/Idris/IDEMode/REPL.idr
M src/Idris/IDEMode/SyntaxHighlight.idr
M src/Idris/IDEMode/TokenLine.idr
M src/Idris/ModTree.idr
M src/Idris/Package.idr
M src/Idris/Package/Init.idr
M src/Idris/Package/Types.idr
M src/Idris/Parser.idr
M src/Idris/Parser/Let.idr
M src/Idris/Pretty.idr
M src/Idris/Pretty/Render.idr
M src/Idris/ProcessIdr.idr
M src/Idris/REPL.idr
M src/Idris/REPL/Common.idr
M src/Idris/REPL/FuzzySearch.idr
M src/Idris/REPL/Opts.idr
M src/Idris/Resugar.idr
M src/Idris/SetOptions.idr
M src/Idris/Syntax.idr
M src/Libraries/Data/Graph.idr
M src/Libraries/Data/IOArray.idr
M src/Libraries/Data/List/Extra.idr
A src/Libraries/Data/List/Quantifiers/Extra.idr
M src/Libraries/Data/NameMap.idr
A src/Libraries/Data/NameMap/Traversable.idr
M src/Libraries/Data/PosMap.idr
A src/Libraries/Data/Span.idr
M src/Libraries/System/Directory/Tree.idr
M src/Libraries/Text/Bounded.idr
M src/Libraries/Text/Distance/Levenshtein.idr
M src/Libraries/Text/Lexer/Core.idr
M src/Libraries/Text/Lexer/Tokenizer.idr
M src/Libraries/Text/Literate.idr
M src/Libraries/Text/Parser.idr
M src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr
M src/Libraries/Text/PrettyPrint/Prettyprinter/Render/HTML.idr
M src/Libraries/Text/PrettyPrint/Prettyprinter/Render/String.idr
M src/Libraries/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr
M src/Libraries/Text/PrettyPrint/Prettyprinter/Util.idr
M src/Libraries/Utils/Binary.idr
M src/Libraries/Utils/Path.idr
M src/Libraries/Utils/Term.idr
M src/Parser/Lexer/Package.idr
M src/Parser/Lexer/Source.idr
M src/Parser/Package.idr
M src/Parser/Rule/Package.idr
M src/Parser/Rule/Source.idr
M src/Parser/Source.idr
M src/Parser/Support.idr
R src/{Libraries/Utils/Hex.idr => Protocol/Hex.idr}
A src/Protocol/IDE.idr
A src/Protocol/IDE/Command.idr
A src/Protocol/IDE/Decoration.idr
A src/Protocol/IDE/FileContext.idr
A src/Protocol/IDE/Formatting.idr
A src/Protocol/IDE/Highlight.idr
A src/Protocol/IDE/Holes.idr
A src/Protocol/IDE/Result.idr
A src/Protocol/SExp.idr
M src/TTImp/BindImplicits.idr
M src/TTImp/Elab.idr
M src/TTImp/Elab/Ambiguity.idr
M src/TTImp/Elab/App.idr
M src/TTImp/Elab/As.idr
M src/TTImp/Elab/Binders.idr
M src/TTImp/Elab/Case.idr
M src/TTImp/Elab/Check.idr
M src/TTImp/Elab/Delayed.idr
M src/TTImp/Elab/Dot.idr
M src/TTImp/Elab/Hole.idr
M src/TTImp/Elab/ImplicitBind.idr
M src/TTImp/Elab/Lazy.idr
M src/TTImp/Elab/Local.idr
M src/TTImp/Elab/Prim.idr
M src/TTImp/Elab/Quote.idr
M src/TTImp/Elab/Record.idr
M src/TTImp/Elab/Rewrite.idr
M src/TTImp/Elab/RunElab.idr
M src/TTImp/Elab/Term.idr
M src/TTImp/Elab/Utils.idr
M src/TTImp/Impossible.idr
M src/TTImp/Interactive/CaseSplit.idr
M src/TTImp/Interactive/ExprSearch.idr
M src/TTImp/Interactive/GenerateDef.idr
M src/TTImp/Interactive/MakeLemma.idr
M src/TTImp/Parser.idr
M src/TTImp/PartialEval.idr
M src/TTImp/ProcessBuiltin.idr
M src/TTImp/ProcessData.idr
M src/TTImp/ProcessDecls.idr
M src/TTImp/ProcessDef.idr
M src/TTImp/ProcessParams.idr
M src/TTImp/ProcessRecord.idr
M src/TTImp/ProcessType.idr
M src/TTImp/Reflect.idr
M src/TTImp/TTImp.idr
M src/TTImp/TTImp/Functor.idr
M src/TTImp/Unelab.idr
M src/TTImp/Utils.idr
M src/Yaffle/Main.idr
M src/Yaffle/REPL.idr
M support/c/Makefile
M support/c/idris_file.c
M support/c/idris_file.h
M support/chez/ct-support.ss
M support/chez/support.ss
M support/gambit/support.scm
M support/racket/ct-support.rkt
M support/racket/support.rkt
M support/refc/Makefile
M tests/Main.idr
M tests/base/data_bits001/BitOps.idr
A tests/base/data_fin001/expected
A tests/base/data_fin001/fromInteger.idr
A tests/base/data_fin001/run
M tests/base/system_file001/ReadFilePage.idr
A tests/base/system_file_fRead/ReadFile.idr
A tests/base/system_file_fRead/expected
A tests/base/system_file_fRead/input
A tests/base/system_file_fRead/run
A tests/base/system_file_fRead/sampleFile.txt
A tests/base/system_file_popen/Popen.idr
A tests/base/system_file_popen/expected
A tests/base/system_file_popen/input
A tests/base/system_file_popen/run
A tests/base/system_run/Run.idr
A tests/base/system_run/expected
A tests/base/system_run/input
A tests/base/system_run/run
M tests/base/system_system/Test.idr
M tests/base/system_system/expected
M tests/chez/chez020/Popen.idr
M tests/chez/chez027/StringParser.idr
M tests/chez/chez027/expected
M tests/chez/integers/TestIntegers.idr
M tests/codegen/builtin001/expected
A tests/contrib/list_alternating/AlternatingList.idr
A tests/contrib/list_alternating/expected
A tests/contrib/list_alternating/input
A tests/contrib/list_alternating/run
M tests/ideMode/ideMode001/expected
M tests/ideMode/ideMode002/expected.in
M tests/ideMode/ideMode003/expected
M tests/ideMode/ideMode004/expected
M tests/ideMode/ideMode005/RecordUpdate.idr
M tests/ideMode/ideMode005/expected1
M tests/ideMode/ideMode005/expected2
M tests/ideMode/ideMode005/expected3
M tests/ideMode/ideMode005/expected4
M tests/ideMode/ideMode005/expected5
M tests/ideMode/ideMode005/expected6
M tests/ideMode/ideMode005/expected7
M tests/ideMode/ideMode005/expected8
M tests/ideMode/ideMode005/expected9
M tests/ideMode/ideMode005/expectedA
M tests/ideMode/ideMode005/expectedB
M tests/ideMode/ideMode005/expectedC
M tests/ideMode/ideMode005/expectedD
M tests/ideMode/ideMode005/expectedE
M tests/ideMode/ideMode005/expectedF
M tests/ideMode/ideMode005/expectedG
M tests/ideMode/ideMode005/expectedH
M tests/idris2/basic003/expected
M tests/idris2/basic005/expected
M tests/idris2/basic016/expected
M tests/idris2/basic042/expected
M tests/idris2/basic049/Fld.idr
M tests/idris2/basic049/expected
A tests/idris2/basic064/Issue2072.idr
A tests/idris2/basic064/expected
A tests/idris2/basic064/input
A tests/idris2/basic064/run
A tests/idris2/basic065/Issue215.idr
A tests/idris2/basic065/expected
A tests/idris2/basic065/run
A tests/idris2/basic066/comment.idr
A tests/idris2/basic066/expected
A tests/idris2/basic066/run
A tests/idris2/basic067/expected
A tests/idris2/basic067/input
A tests/idris2/basic067/run
A tests/idris2/basic067/unclosed1.idr
A tests/idris2/basic067/unclosed2.idr
A tests/idris2/basic067/unclosed3.idr
A tests/idris2/basic068/Issue2138.idr
A tests/idris2/basic068/expected
A tests/idris2/basic068/run
M tests/idris2/docs001/expected
M tests/idris2/error018/expected
A tests/idris2/import007/Mod.idr
A tests/idris2/import007/Mod1.idr
A tests/idris2/import007/Mod2.idr
A tests/idris2/import007/expected
A tests/idris2/import007/run
M tests/idris2/interactive002/expected
M tests/idris2/interactive003/expected
M tests/idris2/interactive009/expected
M tests/idris2/interactive013/expected
M tests/idris2/interactive026/TypeAtRecords.idr
M tests/idris2/interactive026/input
M tests/idris2/interactive028/expected
M tests/idris2/interactive030/expected
M tests/idris2/interactive036/expected
A tests/idris2/interactive038/IEdit.idr
A tests/idris2/interactive038/expected
A tests/idris2/interactive038/input
A tests/idris2/interactive038/run
A tests/idris2/interactive039/CS_Syntax.idr
A tests/idris2/interactive039/expected
A tests/idris2/interactive039/input
A tests/idris2/interactive039/run
A tests/idris2/interactive040/expected
A tests/idris2/interactive040/input
A tests/idris2/interactive040/run
A tests/idris2/interactive041/Issue1741.idr
A tests/idris2/interactive041/expected
A tests/idris2/interactive041/input
A tests/idris2/interactive041/run
A tests/idris2/interpolation004/StringLiteral.idr
A tests/idris2/interpolation004/expected
A tests/idris2/interpolation004/run
A tests/idris2/interpreter008/Issue2041.idr
A tests/idris2/interpreter008/expected
A tests/idris2/interpreter008/input
A tests/idris2/interpreter008/run
M tests/idris2/linear014/run
A tests/idris2/linear015/Issue1861.idr
A tests/idris2/linear015/expected
A tests/idris2/linear015/run
M tests/idris2/literate001/expected
M tests/idris2/literate002/expected
M tests/idris2/literate006/expected
M tests/idris2/literate012/expected
M tests/idris2/literate016/expected
M tests/idris2/params003/expected
A tests/idris2/perf011/A.idr
A tests/idris2/perf011/B.idr
A tests/idris2/perf011/C.idr
A tests/idris2/perf011/expected
A tests/idris2/perf011/run
M tests/idris2/perror007/expected
A tests/idris2/pkg011/dot-slash-dot/Main.idr
A tests/idris2/pkg011/dot-slash-dot/testpkg.ipkg
A tests/idris2/pkg011/dot-slash-name-slash/src/Main.idr
A tests/idris2/pkg011/dot-slash-name-slash/testpkg.ipkg
A tests/idris2/pkg011/dot-slash/Main.idr
A tests/idris2/pkg011/dot-slash/testpkg.ipkg
A tests/idris2/pkg011/dot/Main.idr
A tests/idris2/pkg011/dot/testpkg.ipkg
A tests/idris2/pkg011/expected
A tests/idris2/pkg011/run
A tests/idris2/pkg011/sibling/pkg/testpkg.ipkg
A tests/idris2/pkg011/sibling/src/Main.idr
A tests/idris2/pretty002/SnocList.idr
A tests/idris2/pretty002/expected
A tests/idris2/pretty002/input
A tests/idris2/pretty002/run
M tests/idris2/real001/Channel.idr
M tests/idris2/record002/Record.idr
M tests/idris2/record002/expected
M tests/idris2/record002/input
M tests/idris2/record004/input
M tests/idris2/record005/Fld.idr
A tests/idris2/record010/expected
A tests/idris2/record010/record.idr
A tests/idris2/record010/run
A tests/idris2/record011/Issue2095.idr
A tests/idris2/record011/expected
A tests/idris2/record011/run
A tests/idris2/record012/Issue2065.idr
A tests/idris2/record012/expected
A tests/idris2/record012/run
A tests/idris2/record013/Issue1945.idr
A tests/idris2/record013/expected
A tests/idris2/record013/input
A tests/idris2/record013/run
A tests/idris2/record014/Issue1404.idr
A tests/idris2/record014/expected
A tests/idris2/record014/run
M tests/idris2/reflection004/refdecl.idr
A tests/idris2/reflection012/expected
A tests/idris2/reflection012/input
A tests/idris2/reflection012/nameinfo.idr
A tests/idris2/reflection012/run
A tests/idris2/reflection013/WithUnambig.idr
A tests/idris2/reflection013/expected
A tests/idris2/reflection013/run
A tests/idris2/reflection014/expected
A tests/idris2/reflection014/input
A tests/idris2/reflection014/refdecl.idr
A tests/idris2/reflection014/run
M tests/idris2/reg032/recupdate.idr
M tests/idris2/reg033/DerivingEq.idr
M tests/idris2/reg033/test.idr
M tests/idris2/reg040/expected
M tests/idris2/reg047/QualifiedDoBang.idr
M tests/idris2/reg048/expected
A tests/idris2/schemeeval006/expected
A tests/idris2/schemeeval006/input
A tests/idris2/schemeeval006/run
A tests/idris2/total013/Issue1404.idr
A tests/idris2/total013/expected
A tests/idris2/total013/run
A tests/idris2/warning002/Foo.idr
A tests/idris2/warning002/Main.idr
A tests/idris2/warning002/deprecated.ipkg
A tests/idris2/warning002/expected
A tests/idris2/warning002/run
A tests/idris2/warning003/Main.idr
A tests/idris2/warning003/deprecated.ipkg
A tests/idris2/warning003/expected
A tests/idris2/warning003/run
M tests/idris2/with003/expected
M tests/node/integers/TestIntegers.idr
M tests/node/node020/Popen.idr
A tests/node/nomangle001/expected
A tests/node/nomangle001/nomangle.idr
A tests/node/nomangle001/run
A tests/node/nomangle002/expected
A tests/node/nomangle002/nomangle1.idr
A tests/node/nomangle002/nomangle2.idr
A tests/node/nomangle002/run
M tests/refc/integers/TestIntegers.idr
A tests/refc/refc003/Issue1191.idr
A tests/refc/refc003/expected
A tests/refc/refc003/run
M tests/ttimp/basic003/expected
M tests/ttimp/basic006/expected
M tests/ttimp/coverage002/expected
M tests/ttimp/dot001/expected
M tests/ttimp/eta001/expected
M tests/typedd-book/chapter11/Arith.idr
M tests/typedd-book/chapter11/ArithCmd.idr
M tests/typedd-book/chapter11/ArithCmdDo.idr
M tests/typedd-book/chapter11/ArithTotal.idr
M tests/typedd-book/chapter12/ArithState.idr
This diff is too large to display. Try viewing the raw diff instead.