git.iko.soy/Idris-dev
on master help sign in
Update quasiquoute001 output

This appears to depend on definition ordering in libraries - TCon tag can change.

commitdccd0721a7648c6d9f0a985cb27c7a654e0276d1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 14 Aug 2015, 11:51 (11 years ago) parentbddc058
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 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))))
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))))
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)))