search

thehottgame / TheHoTTGame

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT
125 stars 15 forks source link

Integer Literal confusion #11

Closed russellmcc closed 2 years ago

russellmcc commented 2 years ago

Hi, not familiar with cubical agda, so not sure how to tackle this. In Quest 1 of the fundamental group it was suggested to try sucℤ (- 1) but I get 

1,9-10
ℕ != ℤ
when checking that the expression 1 has type ℤ

sucℤ (- (pos 1)) or sucℤ (negsuc 0) works though - I'm not sure if there's a slicker way to make agda understand that I wanted an integer literal rather than a nat literal

Jlh18 commented 2 years ago

It was our intention to make the user try to interpret our statement according to the definitions. We really intend for the answer here to just be sucℤ ( negsuc zero ), though agda supports sucℤ ( negsuc 0 ) as you pointed out. I think the (slightly messy) way we decided to import things means that you can't do literals for integers, though if you straight up did open import Cubical.Data.Int then you would be able to write sucℤ ( - 1 )

For teaching reasons we wanted some stuff from the library but some stuff from our previous levels

russellmcc commented 2 years ago

Ah, sorry for being unclear, I'm referring to the following passage:

This completes the definition of sucℤ. Use C-c C-n to check it computes correctly. E.g. check that sucℤ (- 1) computes to pos 0 and sucℤ (pos 0) computes to pos 1.

here sucℤ (- 1) does not compute to pos 0 but rather returns an error. Perhaps it would be better to suggest sucℤ (negsuc zero)

Jlh18 commented 2 years ago

Hmm okay. Yeah agree I should be more literal here. Editing...

Jlh18 commented 2 years ago

I think part of the issue is that I used pos 0 and negsuc 0. I should just write pos zero and negsuc zero

russellmcc commented 2 years ago

Similar issues in the following passage

Try computing a few values using C-c C-n, you can try it on refl, loop, loop 3 times, loop (- 1) times and so on.

perhaps this could be

Try computing a few values using C-c C-n, you can try it on refl, loop, loop (pos 3) times, loop (- (pos 1)) times and so on.
Jlh18 commented 2 years ago

- 1 should definitely not be - (pos 1), but instead negsuc zero, since we don't actually define - at any point (but I guess I didn't suppress that import). I might just write english words there instead