Log output from idris-log buffer in Emacs

idris-typechecker.log

 Elaborating Main.SplitView
 Cryptol.idr:83:6
 Main.SplitView pre-type {n : Nat} ->
(m : Nat) ->
Vect (mult m
n)
a ->
Type[]
 Main.SplitView type []
{a : _} ->
{n : Prelude.Nat.Nat} ->
(m : Prelude.Nat.Nat) ->
Main.xyz.Vect (Prelude.Nat.mult m
n)
a ->
Type
 (m : Nat) -> Vect (mult m n) a -> Type
Elaborated: {a : Type 0} -> {n : Prelude.Nat.Nat} -> (m : Prelude.Nat.Nat) -> Main.xyz.Vect (Prelude.Nat.mult m n) a -> Type 0
 Main.SplitView: inaccessible arguments: [(0,a)] from {a : Type ./Cryptol.idr.t15} -> {n : Prelude.Nat.Nat} -> (m : Prelude.Nat.Nat) -> Main.xyz.Vect (Prelude.Nat.mult m n) a -> Type ./Cryptol.idr.z15
{a : _} ->
{n : Prelude.Nat.Nat} ->
(m : Prelude.Nat.Nat) ->
Main.xyz.Vect (Prelude.Nat.mult m
n)
a ->
Type
 Implicit Main.SplitView [PImp {priority = 0, machine_inf = True, argopts = [InaccessibleArg], pname = a, getTm = _},PImp {priority = 1, machine_inf = True, argopts = [], pname = n, getTm = Nat},PExp {priority = 1, argopts = [], pname = m, getTm = Nat},PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = Vect (mult m n) a}]
 Cryptol.idr:84:5:Constructor Main.S : (m : Nat) -> (xs : Vect m (Vect n a)) -> SplitView m (concat xs)
 Main.S pre-type (m : Nat) ->
(xs : Vect m
(Vect n
a)) ->
SplitView m
(Main.concat xs)[]
 Main.S type []
{a : _} ->
{n : _} ->
(m : Prelude.Nat.Nat) ->
(xs : Main.xyz.Vect m
(Main.xyz.Vect n
a)) ->
Main.SplitView {a = _}
{n = _}
m
(Main.concat {a = _}
{n = _}
{m = _}
xs)
 (m : Nat) -> (xs : Vect m (Vect n a)) -> SplitView m (concat xs)
Elaborated: {a : Type 0} -> {n : Prelude.Nat.Nat} -> (m : Prelude.Nat.Nat) -> (xs : Main.xyz.Vect m (Main.xyz.Vect n a)) -> Main.SplitView a n m (Main.concat a n m xs)
 Main.S: inaccessible arguments: [(0,a),(1,n)] from {a : Type ./Cryptol.idr.b16} -> {n : Prelude.Nat.Nat} -> (m : Prelude.Nat.Nat) -> (xs : Main.xyz.Vect m (Main.xyz.Vect n a)) -> Main.SplitView a n m (Main.concat a n m xs)
{a : _} ->
{n : _} ->
(m : Prelude.Nat.Nat) ->
(xs : Main.xyz.Vect m
(Main.xyz.Vect n
a)) ->
Main.SplitView {a = _}
{n = _}
m
(Main.concat {a = _}
{n = _}
{m = _}
xs)
 Implicit Main.S [PImp {priority = 0, machine_inf = True, argopts = [InaccessibleArg], pname = a, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [InaccessibleArg], pname = n, getTm = _},PExp {priority = 1, argopts = [], pname = m, getTm = Nat},PExp {priority = 1, argopts = [], pname = xs, getTm = Vect m (Vect n a)}]
 ---> Main.S : {a : Type ./Cryptol.idr.b16} -> {n : Prelude.Nat.Nat} -> (m : Prelude.Nat.Nat) -> (xs : Main.xyz.Vect m (Main.xyz.Vect n a)) -> Main.SplitView a n m (Main.concat a n m xs)
 Parameters : []
 Elaborating type decl {Main.SplitView_rewrite_lemma0}[]
 {Main.SplitView_rewrite_lemma0} pre-type {x : Main.SplitView left
left} ->
{y : Main.SplitView right
right} ->
(P : {pred : Prelude.Nat.Nat} ->
{pred : Main.xyz.Vect (Prelude.Nat.mult m
n)
a} ->
Main.SplitView pred
pred ->
Type) ->
(=) x
y ->
P y ->
P x[]
 {Main.SplitView_rewrite_lemma0} type []
{a : _} ->
{n : _} ->
{m : _} ->
{right : _} ->
{right : _} ->
{left : _} ->
{left : _} ->
{x : Main.SplitView {a = _}
{n = _}
left
left} ->
{y : Main.SplitView {a = _}
{n = _}
right
right} ->
(P : {pred : Prelude.Nat.Nat} ->
{pred : Main.xyz.Vect (Prelude.Nat.mult m
n)
a} ->
Main.SplitView {a = _}
{n = _}
pred
pred ->
Type) ->
((=) {A = _}
{B = _}
x
y) ->
P y ->
P x