mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2025-01-08 22:30:30 +03:00
99dac56e1e
i.e. if an argument has a polymorphic type, we shouldn't allow a concrete type in its place
8 lines
900 B
Plaintext
8 lines
900 B
Plaintext
Processing as TTImp
|
|
Written TTC
|
|
Yaffle> (Main.Odd (Main.S Main.Z))
|
|
Yaffle> (Main.Even (Main.S Main.Z))
|
|
Yaffle> (Main.Nothing [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) (Main.S Main.Z)) (Main.S (Main.S Main.Z))))])
|
|
Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:9} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))]))
|
|
Yaffle> Bye for now!
|