search

KonjacSource / ShiTT

ShiTT is a toy proof assistant (almost).
BSD 3-Clause "New" or "Revised" License
28 stars 1 forks source link

Absurd Pattern #7

Open KonjacSource opened 3 weeks ago

KonjacSource commented 3 weeks ago 
data N : U where 
| Z : ... 
| S : (_:N) -> ...

data False : U where

data Id {A : U} : (x y : A) -> U where 
| refl : (t : A) -> ... t t 

fun what (add : N -> N -> N) (_ : Id (add Z Z) Z) : False where
| _ k !@ k
KonjacSource commented 3 weeks ago

Adding a new state for unification in pattern matching part, when unifying VCon with a non VCon. In this situation, we are not sure if it possible to use absurd pattern.