Skip to content
Permalink
Browse files

Change definition of cause_type_error

The point is to change it to something that corresponds to a
well-formed piece of concrete syntax, thus making it easier to
explain in a paper.
  • Loading branch information...
IlmariReissumies committed Jun 28, 2019
1 parent 5cd3c1d commit 55bcf9b13e7e80741070b122b1d8599effddd232
Showing with 2 additions and 2 deletions.
  1. +2 −2 characteristic/cfDivScript.sml
@@ -2176,13 +2176,13 @@ val repeat_clos = cfTacticsLib.process_topdecs `

val repeat_body = repeat_clos |> rator |> rand |> rand |> rand |> rand

val cause_type_error_def = Define `cause_type_error = App Opapp []`
val cause_type_error_def = Define `cause_type_error = App Ord [Lit(IntLit 0)]`

Theorem evaluate[simp]:
evaluate s env [cause_type_error] = (s,Rerr (Rabort Rtype_error))
Proof
fs [terminationTheory.evaluate_def,cause_type_error_def,
semanticPrimitivesTheory.do_opapp_def]
semanticPrimitivesTheory.do_opapp_def,semanticPrimitivesTheory.do_app_def]
QED

val then_tyerr_def = Define `then_tyerr e =

0 comments on commit 55bcf9b

Please sign in to comment.
You can’t perform that action at this time.