aya-prover/aya-dev

NullPointerException

ice1000 opened this issue · 1 comments

java.lang.NullPointerException: Cannot invoke "org.aya.syntax.literate.CodeOptions$NormalizeMode.ordinal()" because "<parameter2>" is null
        at aya.base/org.aya.normalize.Normalizer.normalize(Unknown Source)
        at aya.cli.impl/org.aya.cli.interactive.ReplCompiler.lambda$compileToContext$7(Unknown Source)
        at kala.base@0.73.0/kala.control.Either.map(Unknown Source)
        at aya.cli.impl/org.aya.cli.interactive.ReplCompiler.compileToContext(Unknown Source)
        at aya.cli.impl/org.aya.cli.interactive.ReplCompiler.compileToContext(Unknown Source)
        at aya.cli.console/org.aya.cli.repl.AyaRepl.eval(Unknown Source)
        at aya.repl/org.aya.repl.Repl.loop(Unknown Source)
        at aya.cli.console/org.aya.cli.repl.AyaRepl.singleLoop(Unknown Source)
Caused by: java.lang.IndexOutOfBoundsException: Index: 1 Size: 1
	at kala.collection@0.73.0/kala.collection.immutable.ImmutableVectors$Vector1.get(Unknown Source)
	at aya.syntax/org.aya.syntax.compile.JitTele$LocallyNameless.telescope(Unknown Source)
	at aya.syntax/org.aya.syntax.compile.JitTele.telescope(Unknown Source)
	at aya.base/org.aya.unify.TermComparator.compareMany(Unknown Source)
	at aya.base/org.aya.unify.TermComparator.compareCallApprox(Unknown Source)
	at aya.base/org.aya.unify.TermComparator.compareApprox(Unknown Source)
	at aya.base/org.aya.unify.TermComparator.compare(Unknown Source)
	at aya.base/org.aya.tyck.tycker.Unifiable.unifyTerm(Unknown Source)
	at aya.base/org.aya.tyck.tycker.Unifiable.unifyTermReported(Unknown Source)