46bdfa9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Revert quasiquote001

Something about library compilation order? Grump...

commit46bdfa9b897f2ac487a0f6e313aa73ce2f61a48a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 14 Aug 2015, 13:15 (11 years ago) parentdccd072

1 file changed+1−1

compare with master

unifiedsplit

test/quasiquote001/expected+1−1

test/quasiquote001/expected+1−1

@@ -1,5 +1,5 @@

11App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))))

22--------------

3−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 36 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 36 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))

3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))

44--------------

55App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))