<commit_before>module Uninhabited

class Uninhabited t where
  total uninhabited : t -> _|_

instance Uninhabited (Fin Z) where
  uninhabited fZ impossible
  uninhabited (fS f) impossible

instance Uninhabited (Z = S n) where
  uninhabited refl impossible
<commit_msg>Add a function for dealing with absurdity<commit_after>module Uninhabited

class Uninhabited t where
  total uninhabited : t -> _|_

instance Uninhabited (Fin Z) where
  uninhabited fZ impossible
  uninhabited (fS f) impossible

instance Uninhabited (Z = S n) where
  uninhabited refl impossible

-- | Use an absurd assumption to discharge a proof obligation
absurd : Uninhabited t => t -> a
absurd t = FalseElim (uninhabited t)
{'fraction_non_alphanumeric': 0.05603448275862069, 'fraction_numerical': 0.0, 'mean_word_length': 4.488188976377953, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1520164', 'n_tokens_mistral': 233, 'n_tokens_neox': 229, 'n_words': 85}