search

jaccokrijnen / plutus-cert

0 stars 2 forks source link

Kind checking #56

Open TheCodingWombat opened 1 month ago

TheCodingWombat commented 1 month ago

Implemented kind checking.

jaccokrijnen commented 1 month ago

I've added some feedback on the code, it generally looks good :) Could you move the checking code and proofs in a separate coq module? I think src/PlutusIR/Semantics/Static/Kinding/Checker.v would be a logical place.