search

jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.
https://jonsterling.github.io/agda-calf/
Apache License 2.0
54 stars 4 forks source link

Replace U (meta ℕ) with nat #21

Closed HarrisonGrodin closed 3 years ago

jonsterling commented 3 years ago

Honestly, if this works already, then I think we should consider updating the paper because this will be less confusing to the referees. But it's up to y'all.

HarrisonGrodin commented 3 years ago

@jonsterling I'm not sure I follow - I think it's updated in the paper? Here, nat is just defined as U (meta ℕ) in Calf/Types/Nat.agda.

(Although, I think that's a bug in the paper - it says nat = meta ℕ, but should say U (meta ℕ)? cc: @kaonn)

jonsterling commented 3 years ago

Oh LOL, I misunderstood what thisPR was doing. Please ignore me!

kaonn commented 3 years ago

@jonsterling I'm not sure I follow - I think it's updated in the paper? Here, nat is just defined as U (meta ℕ) in Calf/Types/Nat.agda.

(Although, I think that's a bug in the paper - it says nat = meta ℕ, but should say U (meta ℕ)? cc: @kaonn)

Yes I'll fix that.