631afd86 - 6.5610-project

Authored by: Anthony Wang
Authored at: 2026-05-01 14:57:33 -0400
Committed by: Anthony Wang
Committed at: 2026-05-01 14:57:33 -0400
Signature: View
-----BEGIN SSH SIGNATURE----- U1NIU0lHAAAAAQAAADMAAAALc3NoLWVkMjU1MTkAAAAg8Ms9qQOcB6WoVNS51AHxfRPvJz /x6RXeMaql4lvTraUAAAADZ2l0AAAAAAAAAAZzaGE1MTIAAABTAAAAC3NzaC1lZDI1NTE5 AAAAQOAFckMihfcu9Ccyf/VpMqUPTVKfTI+3j5G59mDRXK5H5c1lCAGbNNLA5JWtkRLTXk 8fWar7UcDy5Bj6LqE6DgQ= -----END SSH SIGNATURE-----
Object name: 631afd86d024f145f2e81d676dc749b949683d02
Parent: 2150026d

Fix bug in Lurk port as well

Changes

3 changed files (+6/-2)

Main.lean
- @@ -243,7 +243,7 @@ def evalChk : (env : List Typ) → Env env → (t : Term) → (α : Typ) →
  | _, _, .zero, α, h => by cases α with | nat => exact (0 : Nat) - | new _ => absrdCheck + | new _ => absurdCheck | fn _ _ => absurdCheck | prod _ _ => absurdCheck | sum _ _ => absurdCheck
lakefile.toml
- @@ -1,2 +1,6 @@
  name = "6-5610-project" version = "0.1.0" + + [[lean_exe]] + name = "main" + root = "Main"
main.lurk
- @@ -54,7 +54,7 @@
  (check env (arg1a term) (arg1b term))) ;; False elim (if (and (= (car term) 20n) (eq (car (arg1b term)) 5n)) - t + (check env (arg1a term) (arg1b term)) nil)))))))))) ; Autogenerated by Main.lean