search

wilbowma / cur

A less devious proof assistant
BSD 2-Clause "Simplified" License
222 stars 18 forks source link

sigma doesnt resugar properly #128

Open stchang opened 4 years ago

stchang commented 4 years ago

run ntac/trace with this example (from here: https://github.com/wilbowma/cur/issues/121)

 (ntac/trace
   (∀
    (T : Type)
    (Σ (lst : (List T)) (And (== (List T) lst (nil T)) (Not (== (List T) lst (nil T)))))
    False)
   (by-intros T ex)
   (by-destruct ex #:as [(b H)])
   ...