Skip to content

Instantly share code, notes, and snippets.

@Melvar

Melvar/TestEq.idr

Created May 8, 2015 19:20
Show Gist options
  • Save Melvar/4b26445aeb0242d2d2d5 to your computer and use it in GitHub Desktop.
Save Melvar/4b26445aeb0242d2d2d5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
eqtesteq.txt
Elaborating =
builtin:0:0
= pre-type {A : Type} ->
{B : Type} ->
(x : A) ->
(y : B) ->
Type[]
= type pre-addimpl {A : Type} ->
{B : Type} ->
(x : A) ->
(y : B) ->
Type
= type []
{A : Type} ->
{B : Type} ->
(x : A) ->
(y : B) ->
Type
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty102},Hole {binderTy = Type 0})]
Holes: [{hole1},{ty102},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty102},Hole {binderTy = Type 0})]
Holes: [{hole1},{ty102},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in []
Holes: [{ty102},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty102}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating RType
(EndUnify) Dropping holes: []
SOLVED ({ty102},Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty102}]
Dropping hole {ty102}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty104},Hole {binderTy = Type 0}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{ty104},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty104},Hole {binderTy = Type 0}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{ty104},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{ty104},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty104}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating RType
(EndUnify) Dropping holes: []
SOLVED ({ty104},Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty104}]
Dropping hole {ty104}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty106},Hole {binderTy = Type 0}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole5},{ty106},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty106},Hole {binderTy = Type 0}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole5},{ty106},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{ty106},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty106}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating Var A
(EndUnify) Dropping holes: []
SOLVED ({ty106},A) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty106}]
Dropping hole {ty106}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty108},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole7},{ty108},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty108},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole7},{ty108},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{ty108},{hole7},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty108}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating Var B
(EndUnify) Dropping holes: []
SOLVED ({ty108},B) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty108}]
Dropping hole {ty108}
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(y,Pi {binderImpl = Nothing, binderTy = B, binderKind = Type a}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole7},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{hole7}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating RType
(EndUnify) Dropping holes: []
SOLVED ({hole7},Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole7}]
Dropping hole {hole7}
SOLVED ({hole5},B -> Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole5}]
Dropping hole {hole5}
SOLVED ({hole3},A -> B -> Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole3}]
Dropping hole {hole3}
SOLVED ({hole1},(B : Type 0) -> A -> B -> Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole1}]
Dropping hole {hole1}
SOLVED ({hole0},(A : Type 0) -> (B : Type 0) -> A -> B -> Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole0}]
(EndUnify) Dropping holes: []
Dropping hole {hole0}
Remaining holes:
[]
Remaining problems:
[]
(MatchProblems) Dropping holes: []
(UnifyProblems) Dropping holes: []
A -> B -> Type
Elaborated: (A : Type 0) -> (B : Type 0) -> A -> B -> Type 0
Rechecking
(A : Type 0) -> (B : Type 0) -> A -> B -> Type 0
CONSTRAINTS ADDED: (16,[h <= i,l <= i,k <= l,m <= l,g <= m,n <= m,j <= n,p <= n,o < p,j < k,g < h])
=: inaccessible arguments: [] from (A : Type g) -> (B : Type j) -> A -> B -> Type o
{A : Type} ->
{B : Type} ->
(x : A) ->
(y : B) ->
Type
Implicit = [PImp {priority = 1, machine_inf = True, argopts = [], pname = A, getTm = Type},PImp {priority = 1, machine_inf = True, argopts = [], pname = B, getTm = Type},PExp {priority = 1, argopts = [], pname = x, getTm = A},PExp {priority = 1, argopts = [], pname = y, getTm = B}]
builtin:0:0:Constructor Refl : (x = x)
Refl pre-type {A : Type} ->
{x : A} ->
(=) {A = _}
{B = _}
x
x[]
Refl type pre-addimpl {A : Type} ->
{x : A} ->
(=) {A = _}
{B = _}
x
x
Refl type []
{A : Type} ->
{x : A} ->
(=) {A = _}
{B = _}
x
x
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty102},Hole {binderTy = Type 0})]
Holes: [{hole1},{ty102},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty102},Hole {binderTy = Type 0})]
Holes: [{hole1},{ty102},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in []
Holes: [{ty102},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty102}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating RType
(EndUnify) Dropping holes: []
SOLVED ({ty102},Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty102}]
Dropping hole {ty102}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty104},Hole {binderTy = Type 0}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{ty104},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty104},Hole {binderTy = Type 0}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{ty104},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{ty104},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty104}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating Var A
(EndUnify) Dropping holes: []
SOLVED ({ty104},A) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty104}]
Dropping hole {ty104}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type o,Type 0)
Normalised (Type o,Type 0) in [({y508},Hole {binderTy = {B506}}),({x507},Hole {binderTy = {A505}}),({B506},Hole {binderTy = Type 0}),({A505},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{x507},{y508},{hole1},{hole0},{A505},{B506}]
Injective: []
Unified (Type o,Type 0) without [{y508},{x507},{hole3}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating Var =
(EndUnify) Dropping holes: []
(UnifyProblems) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Elaborating argument (x,{x507},{A505})
Trying (A,{A505})
Normalised (A,{A505}) in [({B506},Hole {binderTy = Type 0}),({A505},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{x507},{hole3},{y508},{hole1},{hole0},{A505},{B506}]
Injective: []
Unified (A,{A505}) without [{x507},{y508},{x507},{hole3}]
Solved: [({A505},A)]
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: [({A505},A)]
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal {A505} -- when elaborating Var x
(EndUnify) Dropping holes: [{A505}]
SOLVED ({x507},x) [{y508},{hole3}]
Updated problems after solve []
(Toplevel) Dropping holes: [{x507}]
Dropping hole {x507}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Elaborating argument (y,{y508},{B506})
Trying (A,{B506})
Normalised (A,{B506}) in [({B506},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{y508},{hole3},{hole1},{hole0},{B506}]
Injective: []
Unified (A,{B506}) without [{y508},{y508},{hole3}]
Solved: [({B506},A)]
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: [({B506},A)]
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal {B506} -- when elaborating Var x
(EndUnify) Dropping holes: [{B506}]
SOLVED ({y508},x) [{hole3}]
Updated problems after solve []
(Toplevel) Dropping holes: [{y508}]
Dropping hole {y508}
SOLVED ({hole3},= A A x x) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole3}]
Dropping hole {hole3}
SOLVED ({hole1},(x : A) -> = A A x x) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole1}]
Dropping hole {hole1}
SOLVED ({hole0},(A : Type 0) -> (x : A) -> = A A x x) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole0}]
(EndUnify) Dropping holes: []
Dropping hole {hole0}
Remaining holes:
[]
Remaining problems:
[]
(MatchProblems) Dropping holes: []
(UnifyProblems) Dropping holes: []
(x = x)
Elaborated: (A : Type 0) -> (x : A) -> = A A x x
Rechecking
(A : Type 0) -> (x : A) -> = A A x x
CONSTRAINTS ADDED: (20,[r <= s,t <= s,q <= t,o <= t,q <= j,q <= g,q < r])
Refl: inaccessible arguments: [] from (A : Type q) -> (x : A) -> = A A x x
{A : Type} ->
{x : A} ->
(=) {A = _}
{B = _}
x
x
Implicit Refl [PImp {priority = 1, machine_inf = True, argopts = [], pname = A, getTm = Type},PImp {priority = 1, machine_inf = True, argopts = [], pname = x, getTm = A}]
builtin:0:0:Constructor Refl elaborated : (x = x)
Inaccessible args: []
---> Refl : (A : Type q) -> (x : A) -> = A A x x
Parameters : []
Raw
eqtestjmeq.txt
data JMEq : {A : Type} ->
{B : Type} -> (x : A) ->
(y : B) -> Type where
| Reflexivity : {A : Type} ->
{x : A} -> JMEq x x
[]
Type checking ./../TestEq.idr
Elaborating JMEq
./../TestEq.idr:3:6
JMEq pre-type {A : Type} ->
{B : Type} ->
(x : A) ->
(y : B) ->
Type[]
JMEq type pre-addimpl {A : Type} ->
{B : Type} ->
(x : A) ->
(y : B) ->
Type
JMEq type []
{A : Type} ->
{B : Type} ->
(x : A) ->
(y : B) ->
Type
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty102},Hole {binderTy = Type 0})]
Holes: [{hole1},{ty102},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty102},Hole {binderTy = Type 0})]
Holes: [{hole1},{ty102},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in []
Holes: [{ty102},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty102}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating RType
(EndUnify) Dropping holes: []
SOLVED ({ty102},Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty102}]
Dropping hole {ty102}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty104},Hole {binderTy = Type 0}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{ty104},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty104},Hole {binderTy = Type 0}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{ty104},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{ty104},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty104}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating RType
(EndUnify) Dropping holes: []
SOLVED ({ty104},Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty104}]
Dropping hole {ty104}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty106},Hole {binderTy = Type 0}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole5},{ty106},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty106},Hole {binderTy = Type 0}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole5},{ty106},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{ty106},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty106}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating Var A
(EndUnify) Dropping holes: []
SOLVED ({ty106},A) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty106}]
Dropping hole {ty106}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty108},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole7},{ty108},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty108},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole7},{ty108},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{ty108},{hole7},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty108}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating Var B
(EndUnify) Dropping holes: []
SOLVED ({ty108},B) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty108}]
Dropping hole {ty108}
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(y,Pi {binderImpl = Nothing, binderTy = B, binderKind = Type a}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(B,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole7},{hole5},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{hole7}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating RType
(EndUnify) Dropping holes: []
SOLVED ({hole7},Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole7}]
Dropping hole {hole7}
SOLVED ({hole5},B -> Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole5}]
Dropping hole {hole5}
SOLVED ({hole3},A -> B -> Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole3}]
Dropping hole {hole3}
SOLVED ({hole1},(B : Type 0) -> A -> B -> Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole1}]
Dropping hole {hole1}
SOLVED ({hole0},(A : Type 0) -> (B : Type 0) -> A -> B -> Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole0}]
(EndUnify) Dropping holes: []
Dropping hole {hole0}
Remaining holes:
[]
Remaining problems:
[]
(MatchProblems) Dropping holes: []
(UnifyProblems) Dropping holes: []
A -> B -> Type
Elaborated: (A : Type 0) -> (B : Type 0) -> A -> B -> Type 0
Rechecking
(A : Type 0) -> (B : Type 0) -> A -> B -> Type 0
CONSTRAINTS ADDED: (30,[v <= w,z <= w,y <= z,a1 <= z,u <= a1,b1 <= a1,x <= b1,d1 <= b1,c1 < d1,x < y,u < v])
JMEq: inaccessible arguments: [] from (A : Type u) -> (B : Type x) -> A -> B -> Type c1
{A : Type} ->
{B : Type} ->
(x : A) ->
(y : B) ->
Type
Implicit JMEq [PImp {priority = 1, machine_inf = True, argopts = [], pname = A, getTm = Type},PImp {priority = 1, machine_inf = True, argopts = [], pname = B, getTm = Type},PExp {priority = 1, argopts = [], pname = x, getTm = A},PExp {priority = 1, argopts = [], pname = y, getTm = B}]
./../TestEq.idr:4:15:Constructor Reflexivity : JMEq x x
Reflexivity pre-type {A : Type} ->
{x : A} ->
JMEq x
x[]
Reflexivity type pre-addimpl {A : Type} ->
{x : A} ->
JMEq x
x
Reflexivity type []
{A : Type} ->
{x : A} ->
JMEq {A = _}
{B = _}
x
x
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty102},Hole {binderTy = Type 0})]
Holes: [{hole1},{ty102},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty102},Hole {binderTy = Type 0})]
Holes: [{hole1},{ty102},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in []
Holes: [{ty102},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty102}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating RType
(EndUnify) Dropping holes: []
SOLVED ({ty102},Type 0) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty102}]
Dropping hole {ty102}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty104},Hole {binderTy = Type 0}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{ty104},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Trying (Type 0,Type a)
Normalised (Type 0,Type a) in [({ty104},Hole {binderTy = Type 0}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{ty104},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type a) without []
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type 0,Type 0)
Normalised (Type 0,Type 0) in [(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{ty104},{hole3},{hole1},{hole0}]
Injective: []
Unified (Type 0,Type 0) without [{ty104}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating Var A
(EndUnify) Dropping holes: []
SOLVED ({ty104},A) []
Updated problems after solve []
(Toplevel) Dropping holes: [{ty104}]
Dropping hole {ty104}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying (Type c1,Type 0)
Normalised (Type c1,Type 0) in [({y508},Hole {binderTy = {B506}}),({x507},Hole {binderTy = {A505}}),({B506},Hole {binderTy = Type 0}),({A505},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{hole3},{x507},{y508},{hole1},{hole0},{A505},{B506}]
Injective: []
Unified (Type c1,Type 0) without [{y508},{x507},{hole3}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal Type 0 -- when elaborating Var JMEq
(EndUnify) Dropping holes: []
(UnifyProblems) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Elaborating argument (x,{x507},{A505})
Trying (A,{A505})
Normalised (A,{A505}) in [({B506},Hole {binderTy = Type 0}),({A505},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{x507},{hole3},{y508},{hole1},{hole0},{A505},{B506}]
Injective: []
Unified (A,{A505}) without [{x507},{y508},{x507},{hole3}]
Solved: [({A505},A)]
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: [({A505},A)]
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal {A505} -- when elaborating Var x
(EndUnify) Dropping holes: [{A505}]
SOLVED ({x507},x) [{y508},{hole3}]
Updated problems after solve []
(Toplevel) Dropping holes: [{x507}]
Dropping hole {x507}
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Elaborating argument (y,{y508},{B506})
Trying (A,{B506})
Normalised (A,{B506}) in [({B506},Hole {binderTy = Type 0}),(x,Pi {binderImpl = Nothing, binderTy = A, binderKind = Type a}),(A,Pi {binderImpl = Nothing, binderTy = Type 0, binderKind = Type a})]
Holes: [{y508},{hole3},{hole1},{hole0},{B506}]
Injective: []
Unified (A,{B506}) without [{y508},{y508},{hole3}]
Solved: [({B506},A)]
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: [({B506},A)]
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal {B506} -- when elaborating Var x
(EndUnify) Dropping holes: [{B506}]
SOLVED ({y508},x) [{hole3}]
Updated problems after solve []
(Toplevel) Dropping holes: [{y508}]
Dropping hole {y508}
SOLVED ({hole3},JMEq A A x x) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole3}]
Dropping hole {hole3}
SOLVED ({hole1},(x : A) -> JMEq A A x x) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole1}]
Dropping hole {hole1}
SOLVED ({hole0},(A : Type 0) -> (x : A) -> JMEq A A x x) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole0}]
(EndUnify) Dropping holes: []
Dropping hole {hole0}
Remaining holes:
[]
Remaining problems:
[]
(MatchProblems) Dropping holes: []
(UnifyProblems) Dropping holes: []
JMEq x x
Elaborated: (A : Type 0) -> (x : A) -> JMEq A A x x
Rechecking
(A : Type 0) -> (x : A) -> JMEq A A x x
CONSTRAINTS ADDED: (34,[f1 <= g1,h1 <= g1,e1 <= h1,c1 <= h1,e1 <= x,e1 <= u,e1 < f1])
Reflexivity: inaccessible arguments: [] from (A : Type e1) -> (x : A) -> JMEq A A x x
{A : Type} ->
{x : A} ->
JMEq {A = _}
{B = _}
x
x
Implicit Reflexivity [PImp {priority = 1, machine_inf = True, argopts = [], pname = A, getTm = Type},PImp {priority = 1, machine_inf = True, argopts = [], pname = x, getTm = A}]
./../TestEq.idr:4:15:Constructor Reflexivity elaborated : JMEq x x
Inaccessible args: []
---> Reflexivity : (A : Type e1) -> (x : A) -> JMEq A A x x
Parameters : []
Rechecking for positivity [JMEq,Reflexivity]
Simplifying {__infer0}
Simplifying Refl
Simplifying Reflexivity
Could not build SCG for {__infer0}
Could not build SCG for Refl
Could not build SCG for Reflexivity
Checking {__infer0} for totality
Constructor {__infer0} is Total with [{__Infer0}]
Checking Refl for totality
Constructor Refl is Total with [=]
Checking Reflexivity for totality
Constructor Reflexivity is Total with [JMEq,Reflexivity]
Totality checking
Totality checking []
Finished ./../TestEq.idr
Universe checking
ALL CONSTRAINTS: fromList [ConstraintFC {uconstraint = a < b, ufc = builtin:0:0},ConstraintFC {uconstraint = c < d, ufc = builtin:0:0},ConstraintFC {uconstraint = e < b, ufc = builtin:0:0},ConstraintFC {uconstraint = g < h, ufc = builtin:0:0},ConstraintFC {uconstraint = j < k, ufc = builtin:0:0},ConstraintFC {uconstraint = o < p, ufc = builtin:0:0},ConstraintFC {uconstraint = q < r, ufc = builtin:0:0},ConstraintFC {uconstraint = s < i, ufc = builtin:0:0},ConstraintFC {uconstraint = u < v, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = x < y, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = c1 < d1, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = e1 < f1, ufc = ./../TestEq.idr:4:15},ConstraintFC {uconstraint = g1 < w, ufc = ./../TestEq.idr:4:15},ConstraintFC {uconstraint = a <= f, ufc = builtin:0:0},ConstraintFC {uconstraint = c <= f, ufc = builtin:0:0},ConstraintFC {uconstraint = d <= e, ufc = builtin:0:0},ConstraintFC {uconstraint = f <= e, ufc = builtin:0:0},ConstraintFC {uconstraint = g <= m, ufc = builtin:0:0},ConstraintFC {uconstraint = h <= i, ufc = builtin:0:0},ConstraintFC {uconstraint = j <= n, ufc = builtin:0:0},ConstraintFC {uconstraint = k <= l, ufc = builtin:0:0},ConstraintFC {uconstraint = l <= i, ufc = builtin:0:0},ConstraintFC {uconstraint = m <= l, ufc = builtin:0:0},ConstraintFC {uconstraint = n <= m, ufc = builtin:0:0},ConstraintFC {uconstraint = o <= t, ufc = builtin:0:0},ConstraintFC {uconstraint = p <= n, ufc = builtin:0:0},ConstraintFC {uconstraint = q <= g, ufc = builtin:0:0},ConstraintFC {uconstraint = q <= j, ufc = builtin:0:0},ConstraintFC {uconstraint = q <= t, ufc = builtin:0:0},ConstraintFC {uconstraint = r <= s, ufc = builtin:0:0},ConstraintFC {uconstraint = t <= s, ufc = builtin:0:0},ConstraintFC {uconstraint = u <= a1, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = v <= w, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = x <= b1, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = y <= z, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = z <= w, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = a1 <= z, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = b1 <= a1, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = c1 <= h1, ufc = ./../TestEq.idr:4:15},ConstraintFC {uconstraint = d1 <= b1, ufc = ./../TestEq.idr:3:6},ConstraintFC {uconstraint = e1 <= u, ufc = ./../TestEq.idr:4:15},ConstraintFC {uconstraint = e1 <= x, ufc = ./../TestEq.idr:4:15},ConstraintFC {uconstraint = e1 <= h1, ufc = ./../TestEq.idr:4:15},ConstraintFC {uconstraint = f1 <= g1, ufc = ./../TestEq.idr:4:15},ConstraintFC {uconstraint = h1 <= g1, ufc = ./../TestEq.idr:4:15}]
Writing ibc "./../TestEq.ibc"
IBCTotal Reflexivity Total 18
IBCTotal Refl Total 17
IBCTotal {__infer0} Total 16
IBCOpt JMEq 15
IBCOpt Reflexivity 14
IBCMetaInformation JMEq (DataMI []) 13
IBCDoc JMEq 12
IBCData JMEq 11
IBCDef JMEq 10
IBCOpt Reflexivity 9
IBCDoc Reflexivity 8
IBCDef Reflexivity 7
IBCImp Reflexivity 6
IBCFnInfo JMEq (FnInfo {fn_params = [0,1]}) 5
IBCImp JMEq 4
IBCParsedRegion ./../TestEq.idr:5:1 3
IBCImportDir "/home/melvar/.cabal/share/x86_64-linux-ghc-7.6.3/idris-0.9.17.1/base" 2
IBCImportDir "/home/melvar/.cabal/share/x86_64-linux-ghc-7.6.3/idris-0.9.17.1/prelude" 1
IBCImportDir "." 0
Written
Skipping ./../TestEq.idr
Loading ibc ./../TestEq.ibc True
Exporting Reflexivity
Exporting JMEq
Exporting []
Raw
eqtesttesteq.txt
*../TestEq> (=)
(=)
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying ({__Infer0},{__Infer0})
Normalised ({__Infer0},{__Infer0}) in [({ival102},Hole {binderTy = {iType101}}),({iType101},Hole {binderTy = Type 0})]
Holes: [{hole0},{ival102},{iType101}]
Injective: []
Unified ({__Infer0},{__Infer0}) without [{ival102},{hole0}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal {__Infer0} -- when elaborating Var {__infer0}
(EndUnify) Dropping holes: []
(UnifyProblems) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Elaborating argument ({ival0},{ival102},{iType101})
Trying ((A : Type g) -> (B : Type j) -> A -> B -> Type o,{iType101})
Normalised ((A : Type g) -> (B : Type j) -> A -> B -> Type o,{iType101}) in [({iType101},Hole {binderTy = Type 0})]
Holes: [{ival102},{hole0},{iType101}]
Injective: []
Unified ((A : Type g) -> (B : Type j) -> A -> B -> Type o,{iType101}) without [{ival102},{ival102},{hole0}]
Solved: [({iType101},(A : Type g) -> (B : Type j) -> A -> B -> Type o)]
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: [({iType101},(A : Type g) -> (B : Type j) -> A -> B -> Type o)]
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal {iType101} -- when elaborating Var =
(EndUnify) Dropping holes: [{iType101}]
(UnifyProblems) Dropping holes: []
SOLVED ({ival102},=) [{hole0}]
Updated problems after solve []
(Toplevel) Dropping holes: [{ival102}]
Dropping hole {ival102}
SOLVED ({hole0},{__infer0} ((A : Type g) -> (B : Type j) -> A -> B -> Type o) =) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole0}]
Dropping hole {hole0}
(EndUnify) Dropping holes: []
Remaining holes:
[]
Remaining problems:
[]
(MatchProblems) Dropping holes: []
(UnifyProblems) Dropping holes: []
Value: =
CONSTRAINTS ADDED: (20,[])
Raw: (=,(A : Type g) -> (B : Type j) -> A -> B -> Type o)
(=) : (A : Type) -> (B : Type) -> A -> B -> Type
Raw
eqtesttestjmeq.txt
*../TestEq> JMEq
JMEq
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying ({__Infer0},{__Infer0})
Normalised ({__Infer0},{__Infer0}) in [({ival102},Hole {binderTy = {iType101}}),({iType101},Hole {binderTy = Type 0})]
Holes: [{hole0},{ival102},{iType101}]
Injective: []
Unified ({__Infer0},{__Infer0}) without [{ival102},{hole0}]
Solved: []
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: []
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal {__Infer0} -- when elaborating Var {__infer0}
(EndUnify) Dropping holes: []
(UnifyProblems) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Elaborating argument ({ival0},{ival102},{iType101})
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Trying ({A503} -> {B504} -> Type `,{iType101})
Normalised ({A503} -> {B504} -> Type `,{iType101}) in [({B504},Hole {binderTy = Type 0}),({A503},Hole {binderTy = Type 0}),({iType101},Hole {binderTy = Type 0})]
Holes: [{ival102},{hole0},{iType101},{A503},{B504}]
Injective: []
Unified ({A503} -> {B504} -> Type `,{iType101}) without [{ival102},{ival102},{hole0}]
Solved: [({iType101},{A503} -> {B504} -> Type `)]
New problems: []
Not unified:
[]
Current problems:
[]
----------
Now solved: [({iType101},{A503} -> {B504} -> Type `)]
Now problems: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Goal {iType101} -- when elaborating Var JMEq
(EndUnify) Dropping holes: [{iType101}]
(UnifyProblems) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
Updated problems after solve []
(Toplevel) Dropping holes: []
SOLVED ({ival102},JMEq {A503} {B504}) [{hole0}]
Updated problems after solve []
(Toplevel) Dropping holes: [{ival102}]
Dropping hole {ival102}
SOLVED ({hole0},{__infer0} ({A503} -> {B504} -> Type `) (JMEq {A503} {B504})) []
Updated problems after solve []
(Toplevel) Dropping holes: [{hole0}]
Dropping hole {hole0}
(EndUnify) Dropping holes: []
Remaining holes:
[{A503},{B504}]
Remaining problems:
[]
(MatchProblems) Dropping holes: []
(UnifyProblems) Dropping holes: []
Value: ? {A503} : Type 0. ? {B504} : Type 0. JMEq {A503} {B504}
Reflecting body of At
Starting error reflection
Using reflection handlers
New error message info:
(input):0:0:Incomplete term JMEq {A = ([__])} {B = ([__])}
Raw
TestEq.idr
%unqualified
data JMEq : {A : Type} -> {B : Type} -> (x : A) -> (y : B) -> Type where
Reflexivity : {A : Type} -> {x : A} -> JMEq x x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment