|
|
|
|
|
|
by perthmad
2332 days ago
|
|
|
You can actually do much better than mere embeddings. Using program translations similar to what Haskell users routinely perform when using the do-notation for monads, you can actually extend your type theory with new reasoning principles. See for instance the parametric exceptional theory [1], which adds well-behaved exceptions and allows to extend Coq with the independence of premises, i.e. (¬A → ∃n:ℕ. P n) → ∃n:ℕ. (¬A → P n). [1] https://hal.inria.fr/hal-01840643/document |
|
|